Questions tagged [functional-extensionality]

Use this tag for the principle of functional extensionality in logic and proofs which states that two functions are equal if their values are equal at every argument.

Filter by
Sorted by
Tagged with
13 votes
2 answers
196 views

Is eta-equality provable in Coq?

Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove ...
user avatar
  • 1,662