diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 28a871bd24fd26d90b48f354a6a0711be2c38c88..4bbbba44af0fd5f9327b806a66585c1c72977ad7 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -623,10 +623,10 @@ Proof. rewrite /Affine=> ->; auto. Qed.
 Global Instance or_affine P Q : Affine P → Affine Q → Affine (P ∨ Q).
 Proof.  rewrite /Affine=> -> ->; auto. Qed.
 Global Instance forall_affine `{Inhabited A} (Φ : A → PROP) :
-  (∀ x, Affine (Φ x)) → Affine (∀ x, Φ x).
+  (∀ x, Affine (Φ x)) → Affine (bi_forall Φ).
 Proof. intros. rewrite /Affine (forall_elim inhabitant). apply: affine. Qed.
 Global Instance exist_affine {A} (Φ : A → PROP) :
-  (∀ x, Affine (Φ x)) → Affine (∃ x, Φ x).
+  (∀ x, Affine (Φ x)) → Affine (bi_exist Φ).
 Proof. rewrite /Affine=> H. apply exist_elim=> a. by rewrite H. Qed.
 
 Global Instance sep_affine P Q : Affine P → Affine Q → Affine (P ∗ Q).
@@ -705,12 +705,12 @@ Proof. intros. by rewrite /Absorbing absorbingly_and_1 !absorbing. Qed.
 Global Instance or_absorbing P Q : Absorbing P → Absorbing Q → Absorbing (P ∨ Q).
 Proof. intros. by rewrite /Absorbing absorbingly_or !absorbing. Qed.
 Global Instance forall_absorbing {A} (Φ : A → PROP) :
-  (∀ x, Absorbing (Φ x)) → Absorbing (∀ x, Φ x).
+  (∀ x, Absorbing (Φ x)) → Absorbing (bi_forall Φ).
 Proof.
   rewrite /Absorbing=> ?. rewrite absorbingly_forall. auto using forall_mono.
 Qed.
 Global Instance exist_absorbing {A} (Φ : A → PROP) :
-  (∀ x, Absorbing (Φ x)) → Absorbing (∃ x, Φ x).
+  (∀ x, Absorbing (Φ x)) → Absorbing (bi_exist Φ).
 Proof.
   rewrite /Absorbing=> ?. rewrite absorbingly_exist. auto using exist_mono.
 Qed.
@@ -1164,13 +1164,13 @@ Global Instance or_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∨ Q).
 Proof. intros. by rewrite /Persistent persistently_or -!persistent. Qed.
 Global Instance forall_persistent `{!BiPersistentlyForall PROP} {A} (Ψ : A → PROP) :
-  (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
+  (∀ x, Persistent (Ψ x)) → Persistent (bi_forall Ψ).
 Proof.
   intros. rewrite /Persistent persistently_forall.
   apply forall_mono=> x. by rewrite -!persistent.
 Qed.
 Global Instance exist_persistent {A} (Ψ : A → PROP) :
-  (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
+  (∀ x, Persistent (Ψ x)) → Persistent (bi_exist Ψ).
 Proof.
   intros. rewrite /Persistent persistently_exist.
   apply exist_mono=> x. by rewrite -!persistent.
diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index cb22e51c877e3ce0a25eb9067f9a1b11a8d2f5d6..f7749031d307efa8778d1fa435f1128b84677b5e 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -384,13 +384,13 @@ Proof.
   rewrite -persistent_and_affinely_sep_l. by apply wand_elim_r'.
 Qed.
 Global Instance forall_timeless {A} (Ψ : A → PROP) :
-  (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
+  (∀ x, Timeless (Ψ x)) → Timeless (bi_forall Ψ).
 Proof.
   rewrite /Timeless=> HQ. rewrite except_0_forall later_forall.
   apply forall_mono; auto.
 Qed.
 Global Instance exist_timeless {A} (Ψ : A → PROP) :
-  (∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).
+  (∀ x, Timeless (Ψ x)) → Timeless (bi_exist Ψ).
 Proof.
   rewrite /Timeless=> ?. rewrite later_exist_false. apply or_elim.
   - rewrite /bi_except_0; auto.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 956586906f448efea5aa41b32919c7ae371967cf..e112d85eee2cad175c5847728b1a8423d4e3da73 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -948,10 +948,10 @@ Section bi_facts.
     rewrite (objective_at Q i). by rewrite (objective_at P k).
   Qed.
   Global Instance forall_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
-    @Objective I PROP (∀ x, Φ x)%I.
+    @Objective I PROP (bi_forall Φ).
   Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
   Global Instance exists_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
-    @Objective I PROP (∃ x, Φ x)%I.
+    @Objective I PROP (bi_exist Φ).
   Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
 
   Global Instance sep_objective P Q `{!Objective P, !Objective Q} :
diff --git a/iris/bi/telescopes.v b/iris/bi/telescopes.v
index 941bac87aee3428122eabf52069e7c849a368ab1..3f3755fb5862bbc883aa01c480a3b69cdb69c512 100644
--- a/iris/bi/telescopes.v
+++ b/iris/bi/telescopes.v
@@ -69,27 +69,27 @@ Section telescopes.
   Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.
 
   Global Instance bi_tforall_absorbing Ψ :
-    (∀ x, Absorbing (Ψ x)) → Absorbing (∀.. x, Ψ x).
+    (∀ x, Absorbing (Ψ x)) → Absorbing (bi_tforall Ψ).
   Proof. rewrite bi_tforall_forall. apply _. Qed.
   Global Instance bi_tforall_persistent `{!BiPersistentlyForall PROP} Ψ :
-    (∀ x, Persistent (Ψ x)) → Persistent (∀.. x, Ψ x).
+    (∀ x, Persistent (Ψ x)) → Persistent (bi_tforall Ψ).
   Proof. rewrite bi_tforall_forall. apply _. Qed.
 
   Global Instance bi_texist_affine Ψ :
-    (∀ x, Affine (Ψ x)) → Affine (∃.. x, Ψ x).
+    (∀ x, Affine (Ψ x)) → Affine (bi_texist Ψ).
   Proof. rewrite bi_texist_exist. apply _. Qed.
   Global Instance bi_texist_absorbing Ψ :
-    (∀ x, Absorbing (Ψ x)) → Absorbing (∃.. x, Ψ x).
+    (∀ x, Absorbing (Ψ x)) → Absorbing (bi_texist Ψ).
   Proof. rewrite bi_texist_exist. apply _. Qed.
   Global Instance bi_texist_persistent Ψ :
-    (∀ x, Persistent (Ψ x)) → Persistent (∃.. x, Ψ x).
+    (∀ x, Persistent (Ψ x)) → Persistent (bi_texist Ψ).
   Proof. rewrite bi_texist_exist. apply _. Qed.
 
   Global Instance bi_tforall_timeless Ψ :
-    (∀ x, Timeless (Ψ x)) → Timeless (∀.. x, Ψ x).
+    (∀ x, Timeless (Ψ x)) → Timeless (bi_tforall Ψ).
   Proof. rewrite bi_tforall_forall. apply _. Qed.
 
   Global Instance bi_texist_timeless Ψ :
-    (∀ x, Timeless (Ψ x)) → Timeless (∃.. x, Ψ x).
+    (∀ x, Timeless (Ψ x)) → Timeless (bi_texist Ψ).
   Proof. rewrite bi_texist_exist. apply _. Qed.
 End telescopes.
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index d6aff23063bf1f658fd3064080a93a625964caa8..222600d2d5ea70d7d5058c4991a689a007f8b9d6 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -20,7 +20,7 @@ Global Hint Extern 0 (FromAssumption _ _ _) =>
 (** Similarly, the lemma [from_exist_exist] is defined using a [Hint Extern] to
 enable the better unification algorithm.
 See https://gitlab.mpi-sws.org/iris/iris/issues/288 *)
-Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
+Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (bi_exist Φ) Φ.
 Proof. by rewrite /FromExist. Qed.
 Global Hint Extern 0 (FromExist _ _) =>
   notypeclasses refine (from_exist_exist _) : typeclass_instances.
@@ -39,14 +39,14 @@ Global Instance as_emp_valid_equiv P Q : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
 Proof. split; [ apply bi.equiv_wand_iff | apply bi.wand_iff_equiv ]. Qed.
 
 Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
-  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀ x, φ x) (∀ x, P x).
+  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀ x, φ x) (bi_forall P).
 Proof.
   rewrite /AsEmpValid=>H1. split=>H2.
   - apply bi.forall_intro=>?. apply H1, H2.
   - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
 Qed.
 Global Instance as_emp_valid_tforall {TT : tele} (φ : TT → Prop) (P : TT → PROP) :
-  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀.. x, φ x) (∀.. x, P x).
+  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀.. x, φ x) (bi_tforall P).
 Proof.
   rewrite /AsEmpValid !tforall_forall bi_tforall_forall.
   apply as_emp_valid_forall.
@@ -132,13 +132,13 @@ Proof.
 Qed.
 
 Global Instance from_assumption_forall {A} p (Φ : A → PROP) Q x :
-  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀ x, Φ x) Q.
+  FromAssumption p (Φ x) Q → KnownLFromAssumption p (bi_forall Φ) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption=> <-.
   by rewrite forall_elim.
 Qed.
 Global Instance from_assumption_tforall {TT : tele} p (Φ : TT → PROP) Q x :
-  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀.. x, Φ x) Q.
+  FromAssumption p (Φ x) Q → KnownLFromAssumption p (bi_tforall Φ) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption=> <-.
   by rewrite bi_tforall_forall forall_elim.
@@ -159,18 +159,18 @@ Global Instance into_pure_pure_impl `{!BiPureForall PROP} (φ1 φ2 : Prop) P1 P2
 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).
-Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
+  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (bi_exist Φ) (ex φ).
+Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. f_equiv=> x. by rewrite Hx. Qed.
 Global Instance into_pure_texist {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
-  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃.. x, Φ x) (∃.. x, φ x).
+  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (bi_texist Φ) (texist φ).
 Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
 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.
+  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (bi_forall Φ) (∀ x, φ x).
+Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. f_equiv=> x. by rewrite Hx. Qed.
 Global Instance into_pure_tforall `{!BiPureForall PROP}
     {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
-  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀.. x, Φ x) (∀.. x, φ x).
+  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (bi_tforall Φ) (tforall φ).
 Proof.
   rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
 Qed.
@@ -257,22 +257,22 @@ Proof.
 Qed.
 
 Global Instance from_pure_exist {A} a (Φ : A → PROP) (φ : A → Prop) :
-  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∃ x, Φ x) (∃ x, φ x).
+  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (bi_exist Φ) (ex φ).
 Proof.
   rewrite /FromPure=>Hx. rewrite pure_exist affinely_if_exist.
   by setoid_rewrite Hx.
 Qed.
 Global Instance from_pure_texist {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
-  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∃.. x, Φ x) (∃.. x, φ x).
+  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (bi_texist Φ) (texist φ).
 Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qed.
 Global Instance from_pure_forall {A} a (Φ : A → PROP) (φ : A → Prop) :
-  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀ x, Φ x) (∀ x, φ x).
+  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (bi_forall Φ) (∀ x, φ x).
 Proof.
-  rewrite /FromPure=>Hx. rewrite pure_forall_1. setoid_rewrite <-Hx.
-  destruct a=>//=. apply affinely_forall.
+  rewrite /FromPure=>Hx. rewrite pure_forall_1.
+  destruct a; simpl in *; rewrite ?affinely_forall; by f_equiv.
 Qed.
 Global Instance from_pure_tforall {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
-  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀.. x, Φ x) (∀.. x, φ x).
+  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (bi_tforall Φ) (tforall φ).
 Proof.
   rewrite /FromPure !tforall_forall bi_tforall_forall. apply from_pure_forall.
 Qed.
@@ -507,10 +507,10 @@ Proof.
 Qed.
 
 Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
-  IntoWand p q (Φ x) P Q → IntoWand p q (∀ x, Φ x) P Q.
+  IntoWand p q (Φ x) P Q → IntoWand p q (bi_forall Φ) P Q.
 Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
 Global Instance into_wand_tforall {TT : tele} p q (Φ : TT → PROP) P Q x :
-  IntoWand p q (Φ x) P Q → IntoWand p q (∀.. x, Φ x) P Q.
+  IntoWand p q (Φ x) P Q → IntoWand p q (bi_tforall Φ) P Q.
 Proof. rewrite /IntoWand=> <-. by rewrite bi_tforall_forall (forall_elim x). Qed.
 
 Global Instance into_wand_affine p q R P Q :
@@ -996,7 +996,7 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (bi_forall Φ) Φ.
 Proof. by rewrite /IntoForall. Qed.
 Global Instance into_forall_tforall {TT : tele} (Φ : TT → PROP) :
-  IntoForall (∀.. a, Φ a) Φ | 10.
+  IntoForall (bi_tforall Φ) Φ | 10.
 Proof. by rewrite /IntoForall bi_tforall_forall. Qed.
 Global Instance into_forall_affinely {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (<affine> P) (λ a, <affine> (Φ a))%I.
@@ -1095,13 +1095,13 @@ Global Instance elim_modal_wandM φ p p' P P' Q Q' mR :
 Proof. rewrite /ElimModal !wandM_sound. exact: elim_modal_wand. Qed.
 Global Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A → PROP) :
   (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) →
-  ElimModal φ p p' P P' (∀ x, Φ x) (∀ x, Ψ x).
+  ElimModal φ p p' P P' (bi_forall Φ) (bi_forall Ψ).
 Proof.
   rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
 Qed.
 Global Instance elim_modal_tforall {TT : tele} φ p p' P P' (Φ Ψ : TT → PROP) :
   (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) →
-  ElimModal φ p p' P P' (∀.. x, Φ x) (∀.. x, Ψ x).
+  ElimModal φ p p' P P' (bi_tforall Φ) (bi_tforall Ψ).
 Proof. rewrite /ElimModal !bi_tforall_forall. apply elim_modal_forall. Qed.
 Global Instance elim_modal_absorbingly_here p P Q :
   Absorbing Q → ElimModal True p false (<absorb> P) P Q Q.
@@ -1121,12 +1121,12 @@ Global Instance add_modal_wandM P P' Q mR :
   AddModal P P' Q → AddModal P P' (mR -∗? Q).
 Proof. rewrite /AddModal wandM_sound. exact: add_modal_wand. Qed.
 Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
-  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀ x, Φ x).
+  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (bi_forall Φ).
 Proof.
   rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
 Global Instance add_modal_tforall {TT : tele} P P' (Φ : TT → PROP) :
-  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀.. x, Φ x).
+  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (bi_tforall Φ).
 Proof. rewrite /AddModal bi_tforall_forall. apply add_modal_forall. Qed.
 
 (** ElimInv *)
diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index 51a84777ddab1afa21cc62f213c0c15f6653826d..fb530108ec503a1ddb9901f8228d3eff3a1d143c 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -327,7 +327,7 @@ Global Instance frame_exist {A} p R (Φ : A → PROP)
     (TT : tele) (g : TT → A) (Ψ : TT → PROP) Q :
   (∀ c, FrameExistRequirements p R Φ (g c) (Ψ c)) →
   TCCbnTele (∃.. c, Ψ c)%I Q →
-  Frame p R (∃ a, Φ a) Q.
+  Frame p R (bi_exist Φ) Q.
 Proof.
   move=> H <-. rewrite /Frame bi_texist_exist.
   eapply frame_exist_helper=> c.
@@ -335,13 +335,13 @@ Proof.
 Qed.
 
 Global Instance frame_texist {TT : tele} p R (Φ Ψ : TT → PROP) :
-  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∃.. x, Φ x) (∃.. x, Ψ x) | 2.
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (bi_texist Φ) (bi_texist Ψ) | 2.
 Proof. rewrite /Frame !bi_texist_exist. apply frame_exist_helper. Qed.
 Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
-  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x) | 2.
+  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (bi_forall Φ) (bi_forall Ψ) | 2.
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 Global Instance frame_tforall {TT : tele} p R (Φ Ψ : TT → PROP) :
-  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∀.. x, Φ x) (∀.. x, Ψ x) | 2.
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (bi_tforall Φ) (bi_tforall Ψ) | 2.
 Proof. rewrite /Frame !bi_tforall_forall. apply frame_forall. Qed.
 
 Global Instance frame_impl_persistent R P1 P2 Q2 :
diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index 6ee58f912c64b1c26450a6cb11e61ef0502ccbdc..a9e0d7cbd9cdf8275b248db972d76d6d7404f626 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -345,11 +345,11 @@ Qed.
 
 Global Instance into_laterN_forall {A} n (Φ Ψ : A → PROP) :
   (∀ x, IntoLaterN false n (Φ x) (Ψ x)) →
-  IntoLaterN false n (∀ x, Φ x) (∀ x, Ψ x).
+  IntoLaterN false n (bi_forall Φ) (bi_forall Ψ).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
 Global Instance into_laterN_exist {A} n (Φ Ψ : A → PROP) :
   (∀ x, IntoLaterN false n (Φ x) (Ψ x)) →
-  IntoLaterN false n (∃ x, Φ x) (∃ x, Ψ x).
+  IntoLaterN false n (bi_exist Φ) (bi_exist Ψ).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
 
 Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index a7047a8e165ae492d86fb5ee0d70090c4592cb04..9aeae150909e7d12c8ab0a2caeab7a19c078b85a 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -472,7 +472,7 @@ Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
 Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
 Proof. by rewrite envs_entails_unseal /IntoIH bi.intuitionistically_elim. Qed.
 Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
-  (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
+  (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (bi_forall Φ) | 2.
 Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
 Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
   IntoIH φ Δ Q → IntoIH (ψ → φ) Δ (⌜ψ⌝ → Q) | 1.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 8f61cdb17c5e6b949fb4b1efb797eff61bf27ce2..d648916f9fa58a07447b07b0fde2ca3f3d01e853 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -107,11 +107,11 @@ Global Instance make_monPred_at_or i P 𝓟 Q 𝓠 :
   MakeMonPredAt i (P ∨ Q) (𝓟 ∨ 𝓠).
 Proof. by rewrite /MakeMonPredAt monPred_at_or=><-<-. Qed.
 Global Instance make_monPred_at_forall {A} i (Φ : A → monPred) (Ψ : A → PROP) :
-  (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → MakeMonPredAt i (∀ a, Φ a) (∀ a, Ψ a).
-Proof. rewrite /MakeMonPredAt monPred_at_forall=>H. by setoid_rewrite <- H. Qed.
+  (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → MakeMonPredAt i (bi_forall Φ) (bi_forall Ψ).
+Proof. rewrite /MakeMonPredAt monPred_at_forall=>H. f_equiv=> ?. by rewrite H. Qed.
 Global Instance make_monPred_at_exists {A} i (Φ : A → monPred) (Ψ : A → PROP) :
-  (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → MakeMonPredAt i (∃ a, Φ a) (∃ a, Ψ a).
-Proof. rewrite /MakeMonPredAt monPred_at_exist=>H. by setoid_rewrite <- H. Qed.
+  (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → MakeMonPredAt i (bi_exist Φ) (bi_exist Ψ).
+Proof. rewrite /MakeMonPredAt monPred_at_exist=>H. f_equiv=> ?. by rewrite H. Qed.
 Global Instance make_monPred_at_persistently i P 𝓟 :
   MakeMonPredAt i P 𝓟 → MakeMonPredAt i (<pers> P) (<pers> 𝓟).
 Proof. by rewrite /MakeMonPredAt monPred_at_persistently=><-. Qed.
@@ -175,12 +175,14 @@ Proof.
 Qed.
 
 Global Instance as_emp_valid_monPred_at φ P (Φ : I → PROP) :
-  AsEmpValid0 φ P → (∀ i, MakeMonPredAt i P (Φ i)) → AsEmpValid φ (∀ i, Φ i) | 100.
+  AsEmpValid0 φ P →
+  (∀ i, MakeMonPredAt i P (Φ i)) →
+  AsEmpValid φ (bi_forall Φ) | 100.
 Proof.
   rewrite /MakeMonPredAt /AsEmpValid0 /AsEmpValid /bi_emp_valid=> -> EQ.
-  setoid_rewrite <-EQ. split.
-  - move=>[H]. apply bi.forall_intro=>i. rewrite -H. by rewrite monPred_at_emp.
-  - move=>HP. split=>i. rewrite monPred_at_emp HP bi.forall_elim //.
+  split.
+  - move=>[H]. apply bi.forall_intro=>i. rewrite -EQ -H monPred_at_emp //.
+  - move=>HP. split=>i. rewrite monPred_at_emp HP EQ bi.forall_elim //.
 Qed.
 Global Instance as_emp_valid_monPred_at_wand φ P Q (Φ Ψ : I → PROP) :
   AsEmpValid0 φ (P -∗ Q) →
@@ -406,10 +408,10 @@ Proof.
   rewrite -assoc bi.impl_elim_l bi.persistently_and_intuitionistically_sep_l. done.
 Qed.
 Global Instance frame_monPred_at_forall {X : Type} p (Ψ : X → monPred) 𝓡 𝓠 i :
-  Frame p 𝓡 (∀ x, Ψ x i) 𝓠 → FrameMonPredAt p i 𝓡 (∀ x, Ψ x) 𝓠.
+  Frame p 𝓡 (∀ x, Ψ x i) 𝓠 → FrameMonPredAt p i 𝓡 (bi_forall Ψ) 𝓠.
 Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_forall. Qed.
 Global Instance frame_monPred_at_exist {X : Type} p (Ψ : X → monPred) 𝓡 𝓠 i :
-  Frame p 𝓡 (∃ x, Ψ x i) 𝓠 → FrameMonPredAt p i 𝓡 (∃ x, Ψ x) 𝓠.
+  Frame p 𝓡 (∃ x, Ψ x i) 𝓠 → FrameMonPredAt p i 𝓡 (bi_exist Ψ) 𝓠.
 Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_exist. Qed.
 
 Global Instance frame_monPred_at_absorbingly p P 𝓡 𝓠 i :