coq - Coq: バインダーでのパラメトリック書き換え

Question

両方が同じパラメーターで使用されるときはいつでもmyeq、述語の下で書き換えたいパラメトリック関係があります。P適切な射を宣言するとうまくいきます:

From Coq Require Import Setoid Morphisms.

Parameter A B : Type.
Parameter myeq : A -> relation B.
Add Parametric Relation (a : A) : B (myeq a) as myeq_rel.

Parameter P : A -> B -> Prop.
Add Parametric Morphism (a : A) : (P a)
    with signature (myeq a) ==> iff as P_morphism.
Admitted.

Lemma test1 b1 b2 :
  (forall a, myeq a b1 b2) ->
  exists a, P a b1.
Proof.
  intro.
  setoid_rewrite H. (* OK *)
Abort.

ただし、関数を適用しようとすると、モーフィズムとして登録されていても機能しなくなりますmyeq。

Parameter Op : B -> B.
Add Parametric Morphism (a : A) : Op
    with signature (myeq a) ==> (myeq a) as op_morphism.
Admitted.

Lemma test2 b1 b2 :
  (forall a, myeq a b1 b2) ->
  exists a, P a (Op b1).
Proof.
  intro.
  setoid_rewrite H. (* not OK, why? *)
Abort.

何かを宣言するのを忘れましたか？