coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof irrelevance for le

From: Julien Forest <forest AT ensiie.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Proof irrelevance for le
Date: Wed, 15 Oct 2008 19:30:49 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=date:from:to:subject:message-id:organization:x-mailer:mime-version :content-type:content-transfer-encoding:sender; b=WSolFP5ZfPYFBI616FjHT9X8A+yvXMQpT7sjDt3nMuWZDhAcy7n40znKBVOsB4SyUv AhGX50gckSOEdl2f8Xm7u2USUoGE1JLf7sReZo1qs2x+TwvycG/XMSN4gK63uto/zvWP NLOYsGaTFYIKQ+2d+9JAxOeOchH4EV/zT6XgM=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: CNAM

Dear all,
I wonder if one can manage to show proof irrelevance for le without
using any axiom nor importing ProofIrrelevance library.

At least, I want to be able to show that le is ProofIrrelevant enough
to be changed in the exist construtor.

Julien

[Coq-Club] Proof irrelevance for le, Julien Forest
- Re: [Coq-Club] Proof irrelevance for le, Pierre Letouzey
- Re: [Coq-Club] Proof irrelevance for le, Frederic Blanqui