coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] dependent induction 2

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Adam Chlipala <adamc AT csail.mit.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] dependent induction 2
Date: Fri, 24 Feb 2012 18:54:14 +0100
Authentication-results: mr.google.com; spf=pass (google.com: domain of pierre.courtieu AT gmail.com designates 10.204.149.198 as permitted sender) smtp.mail=pierre.courtieu AT gmail.com; dkim=pass header.i=pierre.courtieu AT gmail.com

Yes, JMeq_eq is an axiom, I should have make it explicit.
P.C.

2012/2/24 Adam Chlipala
<adamc AT csail.mit.edu>:
> On 02/24/2012 05:07 AM, Pierre Courtieu wrote:
>>
>> Hello, here is a script proving your goal in v8.3 and v8.4 (14975). It
>> makes use of JMeq but the statement of the lemma is the one you want.
>>
>
>
> But the original request asked for an axiom-free proof, right? �Your proof
> uses axiom [JMeq_eq].

[Coq-Club] dependent induction 2, Andrew Polonsky
- Re: [Coq-Club] dependent induction 2, Arnaud Spiwack
- Re: [Coq-Club] dependent induction 2, Pierre Courtieu
  - Re: [Coq-Club] dependent induction 2, Adam Chlipala
    - Re: [Coq-Club] dependent induction 2, Pierre Courtieu
  - Re: [Coq-Club] dependent induction 2, Vincent Siles
    - Re: [Coq-Club] dependent induction 2, Andrew Polonsky