coq-club AT inria.fr

Subject: The Coq mailing list

List archive

rewriting in Type

From: Loic Pottier <Loic.Pottier AT sophia.inria.fr>
To: coq-club AT pauillac.inria.fr
Cc: Benjamin.Werner AT inria.fr
Subject: rewriting in Type
Date: Wed, 20 Jan 1999 10:30:08 +0100
Fax: (33) 93 65 78 58
Organization: INRIA, Sophia Antipolis, France
Telephone: (33) 93 65 78 19

How can I prove this lemma?

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

Lo�c Pottier

rewriting in Type, Loic Pottier
- Re: rewriting in Type, Benjamin Werner