coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Can I prove equality of sigT given its condition?

From: "John Wiegley" <jwiegley AT gmail.com>
To: Daniel Schepler <dschepler AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>, ekmett AT gmail.com
Subject: Re: [Coq-Club] Can I prove equality of sigT given its condition?
Date: Fri, 08 Aug 2014 20:20:35 -0500

>>>>> Daniel Schepler
>>>>> <dschepler AT gmail.com>
>>>>> writes:

> You could maybe restrict the propositional extensionality to the special
> case: forall P:Prop, P -> P = True.

Yes, this works fine, and I see others discussed this axiom back in 2007. I
think I'll just keep admission of it local to the proof and continue on.

Thanks to all,
John

[Coq-Club] Can I prove equality of sigT given its condition?, John Wiegley, 08/08/2014
- Re: [Coq-Club] Can I prove equality of sigT given its condition?, Arthur Azevedo de Amorim, 08/08/2014
  - Re: [Coq-Club] Can I prove equality of sigT given its condition?, gallais, 08/08/2014
- Re: [Coq-Club] Can I prove equality of sigT given its condition?, Adam Chlipala, 08/08/2014
  - Re: [Coq-Club] Can I prove equality of sigT given its condition?, Arthur Azevedo de Amorim, 08/08/2014
  - Re: [Coq-Club] Can I prove equality of sigT given its condition?, John Wiegley, 08/08/2014
    - Re: [Coq-Club] Can I prove equality of sigT given its condition?, Daniel Schepler, 08/08/2014
      - Re: [Coq-Club] Can I prove equality of sigT given its condition?, John Wiegley, 08/09/2014