The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

Lionel Elie Mamane writes:
 > 
 > I was playing around with the notion of equality, and came up with
 > this one:
 > 
 > Inductive myEq:(A,B:Type)A->B->Prop :=
 >  myEq_refl: (C:Type)(x:C) (myEq C C x x).

This is known as John Major's  equality (the origin of this name is to
be found  is C. Mc Bride's  PhD thesis), and  this is part of  the Coq
standard library; see http://coq.inria.fr/library/Coq.Logic.JMeq.html

 > But I can't prove equivalence of myEq and eqT... Is it possible? If
 > not, why? They both look as the smallest reflexive relation to me...

No, it is not provable.

However, Marco Maggesi recently  proved it assuming proof irrelevance.
See http://www.math.unifi.it/~maggesi/coq/jmeq.v

Best regards,
-- 
Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)