New answers tagged functional-extensionality
3
votes
Accepted
Why did this proof succeed without function extensionality?
To expand on @NaïmFavier's answer:
The key here is the difference between definitional and propositional equality.
Most times, when people talk about "function extensionality" they mean ...
- 971
1
vote
Why did this proof succeed without function extensionality?
You don't need function extensionality to prove that, only the $\eta$-rule for functions: then both sides are equal to $\lambda x y.\ f x y$. I don't know if that's how Coq does it.
- 311
Top 50 recent answers are included