coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2.

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: Frederic Blanqui <frederic.blanqui AT inria.fr>
Cc: roconnor AT theorem.ca, Coq Club <coq-club AT pauillac.inria.fr>, sebastien.hinderer AT loria.fr
Subject: Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2.
Date: Fri, 19 Sep 2008 08:44:32 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Frederic Blanqui a �crit :

roconnor AT theorem.ca
a �crit :

I completed a proof of the theorem that le is proof irrelevent, but it
was more difficult than I thought it would be. Does anyone know of a
simpler (axiom-free) proof?

Dear Russel, here is a proof due to Sebastien Hinderer in 2005 available in CoLoR (file Util/Nat/NatUtil.v):

Isn't there a hidden axiom if you use eq_dep_eq ?
Pierre

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Coq-Club] forall n m (H1 H2:le n m), H1=H2., roconnor
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., Frederic Blanqui
  - Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., Pierre Casteran
    - Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., frederic . blanqui
  - Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., S�bastien Hinderer
  - Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., Hugo Herbelin