diff options
| -rw-r--r-- | theories/Logic/FunctionalExtensionality.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index ecb7428e9c..a5894fc1e5 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -19,6 +19,12 @@ Proof. auto. Qed. +Lemma equal_f_dep : forall {A B} {f g : forall (x : A), B x}, + f = g -> forall x, f x = g x. +Proof. +intros A B f g <- H; reflexivity. +Qed. + (** Statements of functional extensionality for simple and dependent functions. *) Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, |