The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

            Hi Loic,

I suggest the following :


Definition proj_sigT :=
[A:Type; P:(A->Type); X:(sigT A P)]
 (sigT_rect A P [_:(sigT A P)]A [a:A; _:(P a)]a X).


And then:

Lemma depidT_idTtype:
      (T, T':Type)
      (P:Type ->Type)
      (f:(P T))
      (g:(P T')) (identityT ? (existT Type P T f) (existT Type P T' g)) ->
      (identityT ? T T').

Intros.
Change (identityT Type (proj_sigT Type P (existT Type P T f))
         (proj_sigT Type P (existT Type P T' g))).
Elim X.
Apply refl_identityT.
Qed.



Note that we need to use "Change" and not the Replace" tactic, since
identity_rect does not exist.



Cheers,



Benjamin