The Coq mailing list

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

On 11/08/2012 06:22 AM, Jesse Clayton wrote:
> Lemma feq: forall (b : K -> K)(c : K -> K)(d : forall g, b g = c g), b 
> = c.
>
> How can this be solved? Is there a predefined library for functions 
> and similar stuff in Coq?

This is a bona fide FAQ. :-)

Short answer: your lemma is actually _not_provable_ in Coq, but many 
users assert it as an axiom.  For more details, see Section 10.6 of CPDT 
<http://adam.chlipala.net/cpdt/>.