The Coq mailing list

[Healfdene Goguen <hhg AT att.com>]

This is somewhat tangential to the discussion of one equality
depending on another, but Conor McBride at Edinburgh has defined a new
equality, the so-called "John Major equality", which allows the types
to be different in the type but not in the introduction rule:

   Inductive jmeq : (A:Type)(B:Type) A -> B -> Prop :=
     jmrefl : (A:Type)(a:A)(jmeq A A a a).

This equality is nice in how it interacts with substitution, since if
you have A : Type, P : A -> Prop and H : (jmeq A A a b), then you
don't need to use a coercion to form (jmeq (P a) (P b) p q) for proofs
p : (P a) and q : (P b).  This is useful when you do inductive proofs
where a and b really are the same thing.

Healf Goguen