The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Wan Hai wrote:
> I want to prove that:
>
> forall m1 m2 n, fc n (fun x=>m1*m2*x) = fc n (fun x=>m2*m1*x)
>
> It is obviously right. [...]
>
> Is there another way to prove this not using the extensionality axiom?
>   

It turns out that (as far as I know), in base CIC without axioms, the 
proposition is not even right, let alone "obviously right." :-)

I think extensionality of functions is logically independent of the 
rules of CIC.  I usually include it as an axiom, but you have to be 
careful about introducing inconsistencies, especially when combining 
with impredicative Set and classical axioms like excluded middle.