The Coq mailing list

[Jesse Clayton <j89clayton89 AT gmail.com>]

Hi,

Variable K : Type.

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?

Thanks.