The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

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).

Basically I wanted to write equality of two terms t1 and t2 without
knowing à-priori that they are of the same type.

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...

The problem I encounter is that "Dependent Rewrite" won't do the job I
thought it would, i.e. under the assumption
(existT Type [x:Type]x A x0)==(existT Type [x:Type]x A x)
replace x by x0 in the goal.

Theorem MyEqEqT:(A:Type)(x,y:A)(myEq ? ? x y) -> (eqT ? x y).
Intros.
Inversion H.
(* Now, in the context there is (among others)
  H3 : (existT Type [x:Type]x A x0)==(existT Type [x:Type]x A x)
  and the goal is:
  x==y
  Why won't the following work?
  *)
Dependent Rewrite <- H4.

(The reciprocate works fine, though. So the question is "Why is myEq
weaker than eqT?")

Thank you for your insight,

-- 
Lionel