Parameter JMeq : forall (A:Type), A -> forall (B:Type), B -> Type. Parameter JMeq_refl : forall (A:Type) (a:A), (JMeq A a A a). Axiom JMeq_elim : forall (A:Type)(a:A)(phi : forall a', JMeq A a A a' -> Type), phi a (JMeq_refl A a) -> forall a' (l:JMeq A a A a'), phi a' l. Lemma JMeq_subst : forall (A:Type) (a:A) (phi : A -> Type), phi a -> forall (b:A) (q: JMeq A a A b), phi b. intros A a phi X b q. generalize q. clear q. apply JMeq_elim with (phi:=fun (a':A) (l:JMeq A a A a') => phi a'). assumption. Qed. Lemma JMeq_unique : forall (A:Type) (a:A) (phi : JMeq A a A a -> Type), phi (JMeq_refl A a) -> forall q:JMeq A a A a, phi q. refine (fun A a phi H l => (JMeq_elim A a (fun (a':A)(l:JMeq A a A a')=> forall (e:JMeq A a A a), JMeq A a' A a -> JMeq (JMeq A a A a') l (JMeq A a A a) e -> phi e) _ a l _ _ _)). intros. eapply JMeq_subst. apply H. assumption. apply JMeq_refl. apply JMeq_refl. Qed.