coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] proof of JMeq_eq

From: maggesi AT math1.unice.fr (Marco.MAGGESI)
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] proof of JMeq_eq
Date: 17 Oct 2002 17:30:33 -0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

I am not sure if this has been already observed, but the axiom JMeq_eq
given in theories/JMeq.v in the standard coq distribution is not too
difficult to prove using eqT_rect (and proof_irrelevance). For those
that are interested I put the proof in

http://www.math.unifi.it/~maggesi/coq/jmeq.v

Marco

[Coq-Club] proof of JMeq_eq, Marco.MAGGESI