Library Coq.Logic.FunctionalExtensionality
This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion.
It introduces a tactic extensionality to apply the axiom of extensionality to an equality goal.
The converse of functional extensionality.
Lemma equal_f :
forall {
A B :
Type} {
f g :
A ->
B},
f = g ->
forall x,
f x = g x.
Statements of functional extensionality for simple and dependent functions.
Apply functional_extensionality, introducing variable x.
Eta expansion follows from extensionality.