The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

http://coq.inria.fr/cocorico/CoqAndAxioms

http://flint.cs.yale.edu/cs430/coq/doc/faq.html#htoc38

kris

On Thu, Nov 8, 2012 at 2:19 PM, Dmitry Grebeniuk 
<gdsfh1 AT gmail.com>
 wrote:
> 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!)