The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

There is an axiom in the FunctionalExtensionality module with signature [ functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g ].  Alternatively, you can use the [extensionality] tactic, which applies a variant of [functional_extensionality].

-Jason

On Thu, Nov 8, 2012 at 6:22 AM, Jesse Clayton <j89clayton89 AT gmail.com> wrote:

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.