Prove forall extensionality

1 files changed, 23 insertions, 1 deletions

diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
index a5894fc1e..14d38c7fb 100644
--- a/theories/Logic/FunctionalExtensionality.v
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -37,13 +37,35 @@ Proof.
   intros ; eauto using @functional_extensionality_dep.
 Qed.
 
+(** Extensionality of [forall]s follows from functional extensionality. *)
+Lemma forall_extensionality {A} {B C : A -> Type} (H : forall x : A, B x = C x)
+: (forall x, B x) = (forall x, C x).
+Proof.
+  apply functional_extensionality in H. destruct H. reflexivity.
+Defined.
+
+Lemma forall_extensionalityP {A} {B C : A -> Prop} (H : forall x : A, B x = C x)
+: (forall x, B x) = (forall x, C x).
+Proof.
+  apply functional_extensionality in H. destruct H. reflexivity.
+Defined.
+
+Lemma forall_extensionalityS {A} {B C : A -> Set} (H : forall x : A, B x = C x)
+: (forall x, B x) = (forall x, C x).
+Proof.
+  apply functional_extensionality in H. destruct H. reflexivity.
+Defined.
+
 (** Apply [functional_extensionality], introducing variable x. *)
 
 Tactic Notation "extensionality" ident(x) :=
   match goal with
     [ |- ?X = ?Y ] =>
     (apply (@functional_extensionality _ _ X Y) ||
-     apply (@functional_extensionality_dep _ _ X Y)) ; intro x
+     apply (@functional_extensionality_dep _ _ X Y) ||
+     apply forall_extensionalityP ||
+     apply forall_extensionalityS ||
+     apply forall_extensionality) ; intro x
   end.
 
 (** Eta expansion follows from extensionality. *)