coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] From equality of foralls to equality of their bodies

From: Edwin Westbrook <westbrook AT kestrel.edu>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] From equality of foralls to equality of their bodies
Date: Fri, 13 Dec 2013 18:20:50 -0800

Hi,

Does anyone know if the following lemma is provable in Coq? I am perfectly
happy to use functional extensionality, or even stronger axioms, as I am
already using informative excluded middle:

Lemma pi_eq_to_app_eq A B B' :
(forall (x:A), B x) = (forall (x:A), B' x) ->
(fun x => B x) = (fun x => B' x).

Thanks in advance!
-Eddy

[Coq-Club] From equality of foralls to equality of their bodies, Edwin Westbrook, 12/14/2013
- Re: [Coq-Club] From equality of foralls to equality of their bodies, Jason Gross, 12/14/2013
  - Re: [Coq-Club] From equality of foralls to equality of their bodies, Edwin Westbrook, 12/16/2013
    - Re: [Coq-Club] From equality of foralls to equality of their bodies, Jason Gross, 12/16/2013
      - Re: [Coq-Club] From equality of foralls to equality of their bodies, Edwin Westbrook, 12/16/2013
        
        Re: [Coq-Club] From equality of foralls to equality of their bodies, Anthony Bordg, 12/17/2013