diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 3afa3312d65f28046c524f10e99bf8b671b30392..b7a6e372142ab0c2457de7b47a8fe8c31eeac952 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -501,8 +501,8 @@ Qed.
 
 Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin uPred_ofe_mixin
   uPred_entails uPred_pure uPred_and uPred_or uPred_impl
-  (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_plainly uPred_persistently
-  (@uPred_internal_eq M) uPred_later.
+  (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
+  uPred_plainly uPred_persistently (@uPred_internal_eq M) uPred_later.
 Proof.
   split.
   - (* Contractive sbi_later *)
@@ -523,9 +523,10 @@ Proof.
     by unseal.
   - (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝ *)
     intros A a b ?. unseal; split=> n x ?; by apply (discrete_iff n).
-  - (* bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q *)
-    unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
-    split; eapply HPQ; eauto using @ucmra_unit_least.
+  - (* bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
+    unseal; split=> n x ? /= HPQ. split=> n' x' ??.
+    move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
+    move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
   - (* Next x ≡ Next y ⊢ ▷ (x ≡ y) *)
     by unseal.
   - (* ▷ (x ≡ y) ⊢ Next x ≡ Next y *)
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 4e8803833affce707c4b92518755583c0cc054b0..ae10b064312182e967f118f2ed3a7c24d4b20c52 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1909,10 +1909,10 @@ Proof.
   rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
 Qed.
 
-Lemma plainly_alt P : bi_plainly P ⊣⊢ P ≡ True.
+Lemma plainly_alt P `{!Absorbing P} : bi_plainly P ⊣⊢ P ≡ True.
 Proof.
   apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply impl_intro_r; auto.
+  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
   - rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly).
     by rewrite plainly_pure True_impl.
 Qed.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 72e484cd7ccab411ccd762200b6bc2f69b80312b..56ef28240860537cdbcf442ddaf8f89b986742b5 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -158,7 +158,7 @@ Section bi_mixin.
     sbi_mixin_fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g;
     sbi_mixin_sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y;
     sbi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝;
-    sbi_mixin_prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢
+    sbi_mixin_prop_ext P Q : bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢
       sbi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
 
     (* Later *)
@@ -261,8 +261,8 @@ Structure sbi := Sbi {
                          sbi_forall sbi_exist sbi_sep sbi_wand sbi_plainly
                          sbi_persistently;
   sbi_sbi_mixin : SbiMixin sbi_ofe_mixin sbi_entails sbi_pure sbi_and sbi_or
-                           sbi_impl sbi_forall sbi_exist sbi_sep sbi_plainly
-                           sbi_persistently sbi_internal_eq sbi_later;
+                           sbi_impl sbi_forall sbi_exist sbi_sep sbi_wand
+                           sbi_plainly sbi_persistently sbi_internal_eq sbi_later;
 }.
 
 Instance: Params (@sbi_later) 1.
@@ -488,7 +488,7 @@ Lemma discrete_eq_1 {A : ofeT} (a b : A) :
   Discrete a → a ≡ b ⊢ (⌜a ≡ b⌝ : PROP).
 Proof. eapply sbi_mixin_discrete_eq_1, sbi_sbi_mixin. Qed.
 
-Lemma prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
+Lemma prop_ext P Q : bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
 Proof. eapply (sbi_mixin_prop_ext _ bi_entails), sbi_sbi_mixin. Qed.
 
 (* Later *)
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index c7bedbc1965f4d4140ae97e71285b0c79c7c169b..36dcb9f0e560aa7b1c40ad81a830887d44a49796 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -345,8 +345,8 @@ Context (I : biIndex) (PROP : sbi).
 Lemma monPred_sbi_mixin :
   SbiMixin (PROP:=monPred I PROP) monPred_ofe_mixin monPred_entails monPred_pure
            monPred_and monPred_or monPred_impl monPred_forall monPred_exist
-           monPred_sep monPred_plainly monPred_persistently monPred_internal_eq
-           monPred_later.
+           monPred_sep monPred_wand monPred_plainly monPred_persistently
+           monPred_internal_eq monPred_later.
 Proof.
   split; unseal.
   - intros n P Q HPQ. split=> i /=.