The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Inductive total2 (T:Type) (P:T -> Type) := tpair: forall t:T, forall x: P t, 
total2 T P.

Inductive total2' (T:Type) (P:T -> Type) := tpair': forall t:T, forall x: P 
t, total2' T P.

Definition pr21 (T:Type) (P:T -> Type) (z: total2 T P) : T := 
match z with 
tpair t x => t
end.  

Lemma a (T:Type)(P:T->Type)(z: total2' T P) : pr21 T P z.


Coq does not understand the lemma saying that z has to be of type total2 T P. 
However, total2 T P and total2' T P are equal (up to alpha equivalence) as 
the terms of the calculus of construction and the membership in one is the 
same as in another. How can I point it out to Coq?

Thanks!
Vladimir.