The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 04/24/2012 07:47 PM, Bernard Hurley wrote:
> 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.
> +++++++++++++++++++++++++++
>    

Short answer: no.

Medium-length answer: keep reading in CPDT. ;)