diff options
Diffstat (limited to 'theories/Logic/FunctionalExtensionality.v')
| -rw-r--r-- | theories/Logic/FunctionalExtensionality.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 5d6a4f7d6..60b71ca33 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -52,5 +52,5 @@ Qed. Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x. Proof. - intros A B f. apply (eta_expansion_dep f). + apply (eta_expansion_dep f). Qed. |