diff --git a/CHANGELOG.md b/CHANGELOG.md
index ae60bff1122111e92065be9bbf05ffb35014e043..2092181bedb570e9ef5864ff6cf716c113a6fb9b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,6 +48,9 @@ With this release, we dropped support for Coq 8.9.
 * Allow framing below an `<affine>` modality if the hypothesis that is framed is
   affine. (Previously, framing below `<affine>` was only possible if the
   hypothesis that is framed resides in the intuitionistic context.)
+* Remove the laws `pure_forall_2 : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI
+  interface and factor it into a type class `BiPureForall`.
+* Add notation `¬ P` for `P → False` to `bi_scope`.
 
 **Changes in `base_logic`:**
 
diff --git a/tests/heapprop.v b/tests/heapprop.v
index e9c0405a23b5c4c38932b98b6e8d2bd7627f9565..9019204c8ca8bde4177a17aebca84d019cc41c7c 100644
--- a/tests/heapprop.v
+++ b/tests/heapprop.v
@@ -149,8 +149,6 @@ Section mixins.
       unseal=> φ P ?; by split.
     - (* [(φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P] *)
       unseal=> φ P HP; split=> σ ?. by apply HP.
-    - (* [(∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝] *)
-      unseal=> A φ; by split.
     - (* [P ∧ Q ⊢ P] *)
       unseal=> P Q; split=> σ [??]; done.
     - (* [P ∧ Q ⊢ Q] *)
@@ -222,6 +220,9 @@ Canonical Structure heapPropI : bi :=
   {| bi_ofe_mixin := ofe_mixin_of heapProp;
      bi_bi_mixin := heapProp_bi_mixin; bi_bi_later_mixin := heapProp_bi_later_mixin |}.
 
+Instance heapProp_pure_forall : BiPureForall heapPropI.
+Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.
+
 Lemma heapProp_proofmode_test {A} (P Q R : heapProp) (Φ Ψ : A → heapProp) :
   P ∗ Q -∗
   □ R -∗
diff --git a/tests/proofmode.v b/tests/proofmode.v
index fd2bbae5b13a7dc40e615956f143a5c40091c644..a7c3a1dc43aa303eef66c3aef6fccca945a075b1 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -215,7 +215,7 @@ Proof.
   Show. auto.
 Qed.
 
-Lemma test_iIntros_pure_not : ⊢@{PROP} ⌜ ¬False ⌝.
+Lemma test_iIntros_pure_not `{!BiPureForall PROP} : ⊢@{PROP} ⌜ ¬False ⌝.
 Proof. by iIntros (?). Qed.
 
 Lemma test_fast_iIntros `{!BiInternalEq PROP} P Q :
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 10807e8566d4d55068802886a6f008481f53ebf0..897592b185c66ebcfe74a977f9d3c7454643a6be 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -27,7 +27,7 @@ Section basic_tests.
   Lemma test_pure_texist {TT : tele} (φ : TT → Prop) :
     (∃.. x, ⌜ φ x ⌝) -∗ ∃.. x, ⌜ φ x ⌝ : PROP.
   Proof. iIntros (H) "!%". done. Qed.
-  Lemma test_pure_tforall {TT : tele} (φ : TT → Prop) :
+  Lemma test_pure_tforall `{!BiPureForall PROP} {TT : tele} (φ : TT → Prop) :
     (∀.. x, ⌜ φ x ⌝) -∗ ∀.. x, ⌜ φ x ⌝ : PROP.
   Proof. iIntros (H) "!%". done. Qed.
   Lemma test_pure_tforall_persistent {TT : tele} (Φ : TT → PROP) :
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 80779bb166483f2d2cd91e59eeec8caa6ec39f8f..261641c77fcd502e479723dfb4caff195b0c749f 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -30,7 +30,6 @@ Proof.
   - exact: persistently_ne.
   - exact: pure_intro.
   - exact: pure_elim'.
-  - exact: @pure_forall_2.
   - exact: and_elim_l.
   - exact: and_elim_r.
   - exact: and_intro.
@@ -90,6 +89,9 @@ Canonical Structure uPredI (M : ucmraT) : bi :=
      bi_bi_mixin := uPred_bi_mixin M;
      bi_bi_later_mixin := uPred_bi_later_mixin M |}.
 
+Instance uPred_pure_forall M : BiPureForall (uPredI M).
+Proof. exact: @pure_forall_2. Qed.
+
 Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
 Proof. apply later_contractive. Qed.
 
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 159f0b964a07c0fb761f84afc934f1f3048b1cee..52ec4bebf2dd7d0fab0891695108aac0bb37336b 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -31,6 +31,8 @@ Notation "(/\)" := bi_and (only parsing) : bi_scope.
 Notation "P \/ Q" := (P ∨ Q)%I (only parsing) : bi_scope.
 Notation "(\/)" := bi_or (only parsing) : bi_scope.
 Notation "P -> Q" := (P → Q)%I (only parsing) : bi_scope.
+Notation "~ P" := (P → False)%I (only parsing) : bi_scope.
+
 Notation "P ** Q" := (P ∗ Q)%I
   (at level 80, right associativity, only parsing) : bi_scope.
 Notation "(**)" := bi_sep (only parsing) : bi_scope.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index f75bddc201a24398327f9daad6738b01af1aacc6..fdeb3a982771514003b786b90575c8b3ae70b39d 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -133,3 +133,12 @@ Arguments löb_weak {_ _} _ _.
 
 Notation BiLaterContractive PROP :=
   (Contractive (bi_later (PROP:=PROP))) (only parsing).
+
+(** The class [BiPureForall] states that universal quantification commutes with
+the embedding of pure propositions. The reverse direction of the entailment
+described by this type class is derivable, so it is not included.
+
+An instance of [BiPureForall] itself is derivable if we assume excluded middle
+in Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
+Class BiPureForall (PROP : bi) :=
+  pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 57a016d07b2ca80e98939edfe5c5b6b29ba6ab65..e9191e1348cd180d4e228335ccadcbe1b41cd4a8 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -526,18 +526,20 @@ Proof.
   - eapply pure_elim=> // -[?|?]; auto using pure_mono.
   - apply or_elim; eauto using pure_mono.
 Qed.
-Lemma pure_impl φ1 φ2 : ⌜φ1 → φ2⌝ ⊣⊢ (⌜φ1⌝ → ⌜φ2⌝).
-Proof.
-  apply (anti_symm _).
-  - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
-  - rewrite -pure_forall_2. apply forall_intro=> ?.
-    by rewrite -(left_id True bi_and (_→_))%I (pure_True φ1) // impl_elim_r.
-Qed.
-Lemma pure_forall {A} (φ : A → Prop) : ⌜∀ x, φ x⌝ ⊣⊢ ∀ x, ⌜φ x⌝.
-Proof.
-  apply (anti_symm _); auto using pure_forall_2.
-  apply forall_intro=> x. eauto using pure_mono.
-Qed.
+Lemma pure_impl_1 φ1 φ2 : ⌜φ1 → φ2⌝ ⊢ (⌜φ1⌝ → ⌜φ2⌝).
+Proof. apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver. Qed.
+Lemma pure_impl_2 `{!BiPureForall PROP} φ1 φ2 : (⌜φ1⌝ → ⌜φ2⌝) ⊢ ⌜φ1 → φ2⌝.
+Proof.
+  rewrite -pure_forall_2. apply forall_intro=> ?.
+  by rewrite -(left_id True bi_and (_→_))%I (pure_True φ1) // impl_elim_r.
+Qed.
+Lemma pure_impl `{!BiPureForall PROP} φ1 φ2 : ⌜φ1 → φ2⌝ ⊣⊢ (⌜φ1⌝ → ⌜φ2⌝).
+Proof. apply (anti_symm _); auto using pure_impl_1, pure_impl_2. Qed.
+Lemma pure_forall_1 {A} (φ : A → Prop) : ⌜∀ x, φ x⌝ ⊢ ∀ x, ⌜φ x⌝.
+Proof. apply forall_intro=> x. eauto using pure_mono. Qed.
+Lemma pure_forall `{!BiPureForall PROP} {A} (φ : A → Prop) :
+  ⌜∀ x, φ x⌝ ⊣⊢ ∀ x, ⌜φ x⌝.
+Proof. apply (anti_symm _); auto using pure_forall_1, pure_forall_2. Qed.
 Lemma pure_exist {A} (φ : A → Prop) : ⌜∃ x, φ x⌝ ⊣⊢ ∃ x, ⌜φ x⌝.
 Proof.
   apply (anti_symm _).
@@ -545,6 +547,13 @@ Proof.
   - apply exist_elim=> x. eauto using pure_mono.
 Qed.
 
+Lemma bi_pure_forall_em : (∀ φ : Prop, φ ∨ ¬φ) → BiPureForall PROP.
+Proof.
+  intros Hem A φ. destruct (Hem (∃ a, ¬φ a)) as [[a Hφ]|Hφ].
+  { rewrite (forall_elim a). by apply pure_elim'. }
+  apply pure_intro=> a. destruct (Hem (φ a)); naive_solver.
+Qed.
+
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
 Proof.
   apply (anti_symm _).
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index b0df9c7573050e5e8485dcbe4f5e9dfd1c4d4170..ba41b1898570fbaa64b031603b60e1da6a7271fb 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -65,9 +65,6 @@ Section bi_mixin.
     (** Higher-order logic *)
     bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝;
     bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P;
-    (* This is actually derivable if we assume excluded middle in Coq,
-       via [(∀ a, φ a) ∨ (∃ a, ¬φ a)]. *)
-    bi_mixin_pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝;
 
     bi_mixin_and_elim_l P Q : P ∧ Q ⊢ P;
     bi_mixin_and_elim_r P Q : P ∧ Q ⊢ Q;
@@ -247,6 +244,7 @@ Notation "(∧)" := bi_and (only parsing) : bi_scope.
 Infix "∨" := bi_or : bi_scope.
 Notation "(∨)" := bi_or (only parsing) : bi_scope.
 Infix "→" := bi_impl : bi_scope.
+Notation "¬ P" := (P → False)%I : bi_scope.
 Infix "∗" := bi_sep : bi_scope.
 Notation "(∗)" := bi_sep (only parsing) : bi_scope.
 Notation "P -∗ Q" := (bi_wand P Q) : bi_scope.
@@ -310,8 +308,6 @@ Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
 Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.
 Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
 Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.
-Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.
-Proof. eapply bi_mixin_pure_forall_2, bi_bi_mixin. Qed.
 
 Lemma and_elim_l P Q : P ∧ Q ⊢ P.
 Proof. eapply bi_mixin_and_elim_l, bi_bi_mixin. Qed.
diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 3297952f2904fecdb955cba33968b988b424d86c..a9eaff530f4ab8081b0f02094ee3cba649c9a1e3 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -9,7 +9,6 @@ Set Default Proof Using "Type*".
 name-dependent allocation. *)
 Module savedprop. Section savedprop.
   Context `{BiAffine PROP}.
-  Notation "¬ P" := (□ (P → False))%I : bi_scope.
   Implicit Types P : PROP.
 
   Context (bupd : PROP → PROP).
@@ -39,15 +38,15 @@ Module savedprop. Section savedprop.
   Qed.
 
   (** A bad recursive reference: "Assertion with name [i] does not hold" *)
-  Definition A (i : ident) : PROP := (∃ P, ¬ P ∗ saved i P)%I.
+  Definition A (i : ident) : PROP := (∃ P, □ ¬ P ∗ saved i P)%I.
 
   Lemma A_alloc : ⊢ |==> ∃ i, saved i (A i).
   Proof. by apply sprop_alloc_dep. Qed.
 
   Lemma saved_NA i : saved i (A i) ⊢ ¬ A i.
   Proof.
-    iIntros "#Hs !> #HA". iPoseProof "HA" as "HA'".
-    iDestruct "HA'" as (P) "[#HNP HsP]". iApply "HNP".
+    iIntros "#Hs #HA". iPoseProof "HA" as "HA'".
+    iDestruct "HA'" as (P) "[HNP HsP]". iApply "HNP".
     iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]".
     { eauto. }
     iApply "HP". done.
@@ -55,8 +54,8 @@ Module savedprop. Section savedprop.
 
   Lemma saved_A i : saved i (A i) ⊢ A i.
   Proof.
-    iIntros "#Hs". iExists (A i). iFrame "#".
-    by iApply saved_NA.
+    iIntros "#Hs". iExists (A i). iFrame "Hs".
+    iIntros "!>". by iApply saved_NA.
   Qed.
 
   Lemma contradiction : False.
@@ -188,14 +187,14 @@ Module inv. Section inv.
   Qed.
 
   (** And now we tie a bad knot. *)
-  Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : bi_scope.
-  Definition A i : PROP := (∃ P, ¬P ∗ saved i P)%I.
+  Notation not_fupd P := (□ (P -∗ fupd M1 False))%I.
+  Definition A i : PROP := (∃ P, not_fupd P ∗ saved i P)%I.
   Global Instance A_persistent i : Persistent (A i) := _.
 
   Lemma A_alloc : ⊢ fupd M1 (∃ i, saved i (A i)).
   Proof. by apply saved_alloc. Qed.
 
-  Lemma saved_NA i : saved i (A i) ⊢ ¬A i.
+  Lemma saved_NA i : saved i (A i) ⊢ not_fupd (A i).
   Proof.
     iIntros "#Hi !> #HA". iPoseProof "HA" as "HA'".
     iDestruct "HA'" as (P) "#[HNP Hi']".
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index f5a13ea1733f7d69465865d9be22fa57e5024078..a81009a0d9ea3624793303846878a175cd6b490b 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -259,7 +259,6 @@ Proof.
     + intros [[] []]. split=>i. by apply bi.equiv_spec.
   - intros P φ ?. split=> i. by apply bi.pure_intro.
   - intros φ P HP. split=> i. apply bi.pure_elim'=> ?. by apply HP.
-  - intros A φ. split=> i. by apply bi.pure_forall_2.
   - intros P Q. split=> i. by apply bi.and_elim_l.
   - intros P Q. split=> i. by apply bi.and_elim_r.
   - intros P Q R [?] [?]. split=> i. by apply bi.and_intro.
@@ -402,6 +401,9 @@ Proof. unseal. split. solve_proper. Qed.
 Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
 Proof. solve_proper. Qed.
 
+Global Instance monPred_pure_forall : BiPureForall PROP → BiPureForall monPredI.
+Proof. intros ? A φ. split=> /= i. unseal. by apply pure_forall_2. Qed.
+
 Global Instance monPred_later_contractive :
   BiLaterContractive PROP → BiLaterContractive monPredI.
 Proof. unseal=> ? n P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 2ee7a4d62d986402a54cb9d7f2c4911cfb90ca3b..6f2af1ea3b4b02b6910f4179ae3b7a0ca4592619 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -155,9 +155,9 @@ Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
 Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∨ P2) (φ1 ∨ φ2).
 Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
-Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
+Global Instance into_pure_pure_impl `{!BiPureForall PROP} (φ1 φ2 : Prop) P1 P2 :
   FromPure false P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 → P2) (φ1 → φ2).
-Proof. rewrite /FromPure /IntoPure pure_impl=> <- -> //. Qed.
+Proof. rewrite /FromPure /IntoPure /= => <- ->. apply pure_impl_2. Qed.
 
 Global Instance into_pure_exist {A} (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃ x, Φ x) (∃ x, φ x).
@@ -165,10 +165,12 @@ Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
 Global Instance into_pure_texist {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃.. x, Φ x) (∃.. x, φ x).
 Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
-Global Instance into_pure_forall {A} (Φ : A → PROP) (φ : A → Prop) :
+Global Instance into_pure_forall `{!BiPureForall PROP}
+    {A} (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀ x, Φ x) (∀ x, φ x).
 Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
-Global Instance into_pure_tforall {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
+Global Instance into_pure_tforall `{!BiPureForall PROP}
+    {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀.. x, Φ x) (∀.. x, φ x).
 Proof.
   rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
@@ -177,7 +179,7 @@ Qed.
 Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∗ P2) (φ1 ∧ φ2).
 Proof. rewrite /IntoPure=> -> ->. by rewrite sep_and pure_and. Qed.
-Global Instance into_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
+Global Instance into_pure_pure_wand `{!BiPureForall PROP} a (φ1 φ2 : Prop) P1 P2 :
   FromPure a P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2).
 Proof.
   rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
@@ -218,7 +220,7 @@ Qed.
 Global Instance from_pure_pure_impl a (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → FromPure a P2 φ2 → FromPure a (P1 → P2) (φ1 → φ2).
 Proof.
-  rewrite /FromPure /IntoPure pure_impl=> -> <-. destruct a=>//=.
+  rewrite /FromPure /IntoPure pure_impl_1=> -> <-. destruct a=>//=.
   apply bi.impl_intro_l. by rewrite affinely_and_r bi.impl_elim_r.
 Qed.
 
@@ -234,7 +236,7 @@ Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qe
 Global Instance from_pure_forall {A} a (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀ x, Φ x) (∀ x, φ x).
 Proof.
-  rewrite /FromPure=>Hx. rewrite pure_forall. setoid_rewrite <-Hx.
+  rewrite /FromPure=>Hx. rewrite pure_forall_1. setoid_rewrite <-Hx.
   destruct a=>//=. apply affinely_forall.
 Qed.
 Global Instance from_pure_tforall {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
@@ -260,8 +262,8 @@ Proof.
   destruct a; simpl.
   - destruct Ha as [Ha|?]; first inversion Ha.
     rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
-    by rewrite affinely_and_l pure_impl impl_elim_r.
-  - by rewrite HP1 sep_and pure_impl impl_elim_r.
+    by rewrite affinely_and_l pure_impl_1 impl_elim_r.
+  - by rewrite HP1 sep_and pure_impl_1 impl_elim_r.
 Qed.
 
 Global Instance from_pure_persistently P a φ :
@@ -880,15 +882,16 @@ Proof. by rewrite /FromForall. Qed.
 Global Instance from_forall_tforall {TT : tele} (Φ : TT → PROP) name :
   AsIdentName Φ name → FromForall (bi_tforall Φ) Φ name.
 Proof. by rewrite /FromForall bi_tforall_forall. Qed.
-Global Instance from_forall_pure {A} (φ : A → Prop) name :
+Global Instance from_forall_pure `{!BiPureForall PROP} {A} (φ : A → Prop) name :
   AsIdentName φ name → @FromForall PROP A ⌜∀ a : A, φ a⌝ (λ a, ⌜ φ a ⌝)%I name.
-Proof. by rewrite /FromForall pure_forall. Qed.
-Global Instance from_tforall_pure {TT : tele} (φ : TT → Prop) name :
+Proof. by rewrite /FromForall pure_forall_2. Qed.
+Global Instance from_tforall_pure `{!BiPureForall PROP}
+    {TT : tele} (φ : TT → Prop) name :
   AsIdentName φ name → @FromForall PROP TT ⌜tforall φ⌝ (λ x, ⌜ φ x ⌝)%I name.
 Proof. by rewrite /FromForall tforall_forall pure_forall. Qed.
 
 (* [H] is the default name for the [φ] hypothesis, in the following three instances *)
-Global Instance from_forall_pure_not (φ : Prop) :
+Global Instance from_forall_pure_not `{!BiPureForall PROP} (φ : Prop) :
   @FromForall PROP φ ⌜¬ φ⌝ (λ _ : φ, False)%I (to_ident_name H).
 Proof. by rewrite /FromForall pure_forall. Qed.
 Global Instance from_forall_impl_pure P Q φ :
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index d9cc4ae66a4a4c5ef2d824f0d3be2927efbdccf4..baa2514ea02660585ce60420dc38a5fe1e233a63 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -37,7 +37,6 @@ Proof.
   - solve_proper.
   - exact: pure_intro.
   - exact: pure_elim'.
-  - exact: @pure_forall_2.
   - exact: and_elim_l.
   - exact: and_elim_r.
   - exact: and_intro.
@@ -116,6 +115,9 @@ Canonical Structure siPropI : bi :=
   {| bi_ofe_mixin := ofe_mixin_of siProp;
      bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}.
 
+Instance siProp_pure_forall : BiPureForall siPropI.
+Proof. exact: @pure_forall_2. Qed.
+
 Instance siProp_later_contractive : BiLaterContractive siPropI.
 Proof. apply later_contractive. Qed.