The Coq mailing list

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

±èÇü¼± wrote:
>
> I am cautious about assuming the following:
>
> Axiom fun_eq : forall (A B : Type) (f g: A -> B) (a : A), (forall a :
> A, f a = g a) -> f = g.
>
> [...]
>
> What are expected dangers of assuming each?
>

Your first axiom is already in the Coq standard library, so it would be
better to import that module than to redefine the axiom:
http://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html
A section of the FAQ addresses its consistency:
http://coq.inria.fr/faq?som=5#htoc41