The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

Hello.

> 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/>.

  But there are no explanations about why the functional
extensionality is not used by default (for "auto" tactic,
for example; moveover, requires explicit Require Import).
So, are there any cases when this axiom is undesirable?
Can it break something?  I'd be glad to know about it (either
in coq-club or from CPDT).
  (btw, your book is great!)