The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Have you seen:

http://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html

??

On Tue, Apr 24, 2012 at 7:47 PM, Bernard Hurley 
<bernard AT marcade.biz>
 wrote:
> Hi all,
>
> In the following scenario, is it possible to prove the Lemma?
>
> +++++++++++++++++++++++++++
> Section test.
>  Variables A B : Set.
>  Variables f g : A -> B.
>
>  Hypothesis Hyp1: forall a, f a = g a.
>
>  Lemma test : f = g.
>
> End test.
> +++++++++++++++++++++++++++
>
> The hypothesis is just the normal mathematical definition of the
> equality of two functions. But I can't figure out whether it is
> reasonable to expect to be able to prove the Lemma or whether one would
> need and extra axiom.
>
> Thanks,
>
> Bernard.
>