diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 996e434bf4b352ddc13ab0294b309bc5b43681e9..dd997c89eb15b3a01b24f36c4b4933a1892ff76f 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -2306,12 +2306,12 @@ Section bi_morphims.
   Global Instance bi_mor_mono_flip : Proper (flip (⊢) ==> flip (⊢)) mor.
   Proof. solve_proper. Qed.
 
-  Lemma bi_mor_forall A Φ : mor (@bi_forall _ A Φ) ⊣⊢ (∀ x, mor (Φ x)).
+  Lemma bi_mor_forall A (Φ : A → PROP1) : mor (∀ x, Φ x) ⊣⊢ (∀ x, mor (Φ x)).
   Proof.
     apply bi.equiv_spec; split; [|apply bi_mor_forall_2].
     apply bi.forall_intro=>?. by rewrite bi.forall_elim.
   Qed.
-  Lemma bi_mor_exist A Φ : mor (@bi_exist _ A Φ) ⊣⊢ (∃ x, mor (Φ x)).
+  Lemma bi_mor_exist A (Φ : A → PROP1) : mor (∃ x, Φ x) ⊣⊢ (∃ x, mor (Φ x)).
   Proof.
     apply bi.equiv_spec; split; [apply bi_mor_exist_1|].
     apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 18bc2ad2aef39b5dbdc03938b9ce0d5b77a58425..e756e90583cfa2258651d35986a5c092bf3372b4 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -342,8 +342,8 @@ Class BiMorphism {PROP1 PROP2 : bi} (f : PROP1 → PROP2) := {
   bi_mor_mono :> Proper ((⊢) ==> (⊢)) f;
   bi_mor_emp : f emp ⊣⊢ emp;
   bi_mor_impl_2 P Q : (f P → f Q)%I ⊢ f (P → Q)%I;
-  bi_mor_forall_2 A Φ : (∀ x, f (Φ x)) ⊢ f (@bi_forall _ A Φ);
-  bi_mor_exist_1 A Φ : f (@bi_exist _ A Φ) ⊢ ∃ x, f (Φ x);
+  bi_mor_forall_2 A (Φ : A → PROP1) : (∀ x, f (Φ x)) ⊢ f (∀ x, Φ x);
+  bi_mor_exist_1 A (Φ : A → PROP1) : f (∃ x, Φ x) ⊢ ∃ x, f (Φ x);
   bi_mor_internal_eq_1 (A : ofeT) (x y : A) : f (x ≡ y) ⊢ (x ≡ y);
   bi_mor_sep P Q : f (P ∗ Q) ⊣⊢ (f P ∗ f Q);
   bi_mor_wand_2 P Q : (f P -∗ f Q) ⊢ f (P -∗ Q);