The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

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.