From 50b10db2d49aa1df59b008750272c27f4522ea42 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 26 Mar 2023 15:37:20 +0200
Subject: [PATCH] Indent some sections.

---
 iris/bi/internal_eq.v |  340 +++++++-------
 iris/bi/plainly.v     | 1034 ++++++++++++++++++++---------------------
 2 files changed, 687 insertions(+), 687 deletions(-)

diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 1353e7ddf..c5020d48e 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -79,175 +79,175 @@ End internal_eq_laws.
 
 (* Derived laws *)
 Section internal_eq_derived.
-Context {PROP : bi} `{!BiInternalEq PROP}.
-Implicit Types P : PROP.
-
-(* Force implicit argument PROP *)
-Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
-Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
-
-Global Instance internal_eq_proper (A : ofe) :
-  Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A) := ne_proper_2 _.
-
-(* Equality *)
-Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
-Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
-Local Hint Resolve internal_eq_refl : core.
-Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
-
-Lemma equiv_internal_eq {A : ofe} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
-Proof. intros ->. auto. Qed.
-Lemma internal_eq_rewrite' {A : ofe} a b (Ψ : A → PROP) P
-  {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
-  intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
-  apply impl_elim_l'. by apply internal_eq_rewrite.
-Qed.
-
-Lemma internal_eq_sym {A : ofe} (a b : A) : a ≡ b ⊢ b ≡ a.
-Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
-Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
-Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.
-
-Lemma f_equivI {A B : ofe} (f : A → B) `{!NonExpansive f} x y :
-  x ≡ y ⊢ f x ≡ f y.
-Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
-Lemma f_equivI_contractive {A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
-  ▷ (x ≡ y) ⊢ f x ≡ f y.
-Proof.
-  rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg.
-  by apply f_equivI.
-Qed.
-
-Lemma prod_equivI {A B : ofe} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
-Proof.
-  apply (anti_symm _).
-  - apply and_intro; apply f_equivI; apply _.
-  - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
-    apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
-    apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
-Qed.
-Lemma sum_equivI {A B : ofe} (x y : A + B) :
-  x ≡ y ⊣⊢
-    match x, y with
-    | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
-    end.
-Proof.
-  apply (anti_symm _).
-  - apply (internal_eq_rewrite' x y (λ y,
-             match x, y with
-             | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
-             end)%I); auto.
-    destruct x; auto.
-  - destruct x as [a|b], y as [a'|b']; auto; apply f_equivI, _.
-Qed.
-Lemma option_equivI {A : ofe} (x y : option A) :
-  x ≡ y ⊣⊢ match x, y with
-           | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
-           end.
-Proof.
-  apply (anti_symm _).
-  - apply (internal_eq_rewrite' x y (λ y,
-             match x, y with
+  Context {PROP : bi} `{!BiInternalEq PROP}.
+  Implicit Types P : PROP.
+
+  (* Force implicit argument PROP *)
+  Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+  Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
+
+  Global Instance internal_eq_proper (A : ofe) :
+    Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A) := ne_proper_2 _.
+
+  (* Equality *)
+  Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
+  Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
+  Local Hint Resolve internal_eq_refl : core.
+  Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
+
+  Lemma equiv_internal_eq {A : ofe} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
+  Proof. intros ->. auto. Qed.
+  Lemma internal_eq_rewrite' {A : ofe} a b (Ψ : A → PROP) P
+    {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+  Proof.
+    intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
+    apply impl_elim_l'. by apply internal_eq_rewrite.
+  Qed.
+
+  Lemma internal_eq_sym {A : ofe} (a b : A) : a ≡ b ⊢ b ≡ a.
+  Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
+  Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
+  Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.
+
+  Lemma f_equivI {A B : ofe} (f : A → B) `{!NonExpansive f} x y :
+    x ≡ y ⊢ f x ≡ f y.
+  Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
+  Lemma f_equivI_contractive {A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
+    ▷ (x ≡ y) ⊢ f x ≡ f y.
+  Proof.
+    rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg.
+    by apply f_equivI.
+  Qed.
+
+  Lemma prod_equivI {A B : ofe} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
+  Proof.
+    apply (anti_symm _).
+    - apply and_intro; apply f_equivI; apply _.
+    - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
+      apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
+      apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
+  Qed.
+  Lemma sum_equivI {A B : ofe} (x y : A + B) :
+    x ≡ y ⊣⊢
+      match x, y with
+      | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
+      end.
+  Proof.
+    apply (anti_symm _).
+    - apply (internal_eq_rewrite' x y (λ y,
+               match x, y with
+               | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
+               end)%I); auto.
+      destruct x; auto.
+    - destruct x as [a|b], y as [a'|b']; auto; apply f_equivI, _.
+  Qed.
+  Lemma option_equivI {A : ofe} (x y : option A) :
+    x ≡ y ⊣⊢ match x, y with
              | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
-             end)%I); auto.
-    destruct x; auto.
-  - destruct x as [a|], y as [a'|]; auto. apply f_equivI, _.
-Qed.
-
-Lemma sig_equivI {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
-Proof.
-  apply (anti_symm _).
-  - apply sig_equivI_1.
-  - apply f_equivI, _.
-Qed.
-
-Section sigT_equivI.
-Import EqNotations.
-
-Lemma sigT_equivI {A : Type} {P : A → ofe} (x y : sigT P) :
-  x ≡ y ⊣⊢
-  ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
-Proof.
-  apply (anti_symm _).
-  - apply (internal_eq_rewrite' x y (λ y,
-             ∃ eq : projT1 x = projT1 y,
-               rew eq in projT2 x ≡ projT2 y))%I;
-        [| done | exact: (exist_intro' _ _ eq_refl) ].
-    move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
-    apply exist_ne => ?. by rewrite Hab.
-  - apply exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
-    apply f_equivI, _.
-Qed.
-End sigT_equivI.
-
-Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-Proof.
-  apply (anti_symm _); auto using fun_extI.
-  apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
-Qed.
-Lemma ofe_morO_equivI {A B : ofe} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-Proof.
-  apply (anti_symm _).
-  - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
-  - rewrite -(discrete_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
-    set (h1 (f : A -n> B) :=
-      exist (λ f : A -d> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
-    set (h2 (f : sigO (λ f : A -d> B, NonExpansive (f : A → B))) :=
-      @OfeMor A B (`f) (proj2_sig f)).
-    assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []).
-    assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
-    by rewrite -{2}[f]Hh -{2}[g]Hh -f_equivI -sig_equivI.
-Qed.
-
-Lemma pure_internal_eq {A : ofe} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y.
-Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
-Lemma discrete_eq {A : ofe} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝.
-Proof.
-  intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
-Qed.
-
-Lemma absorbingly_internal_eq {A : ofe} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
-Proof.
-  apply (anti_symm _), absorbingly_intro.
-  apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
-  apply wand_intro_l, internal_eq_refl.
-Qed.
-Lemma persistently_internal_eq {A : ofe} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
-  apply (anti_symm (⊢)).
-  { by rewrite persistently_into_absorbingly absorbingly_internal_eq. }
-  apply (internal_eq_rewrite' a b (λ b, <pers> (a ≡ b))%I); auto.
-  rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
-Qed.
-
-Global Instance internal_eq_absorbing {A : ofe} (x y : A) :
-  Absorbing (PROP:=PROP) (x ≡ y).
-Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
-Global Instance internal_eq_persistent {A : ofe} (a b : A) :
-  Persistent (PROP:=PROP) (a ≡ b).
-Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
-
-(* Equality under a later. *)
-Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP)
-  {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
-Proof.
-  rewrite f_equivI_contractive. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
-Qed.
-Lemma internal_eq_rewrite_contractive' {A : ofe} a b (Ψ : A → PROP) P
-  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
-  rewrite later_equivI_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
-  by apply internal_eq_rewrite'.
-Qed.
-
-Lemma later_equivI {A : ofe} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
-Proof. apply (anti_symm _); auto using later_equivI_1, later_equivI_2. Qed.
-Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q :
-  ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
-Proof. apply (f_equivI_contractive _). Qed.
-
-Global Instance eq_timeless {A : ofe} (a b : A) :
-  Discrete a → Timeless (PROP:=PROP) (a ≡ b).
-Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
+             end.
+  Proof.
+    apply (anti_symm _).
+    - apply (internal_eq_rewrite' x y (λ y,
+               match x, y with
+               | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
+               end)%I); auto.
+      destruct x; auto.
+    - destruct x as [a|], y as [a'|]; auto. apply f_equivI, _.
+  Qed.
+
+  Lemma sig_equivI {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
+  Proof.
+    apply (anti_symm _).
+    - apply sig_equivI_1.
+    - apply f_equivI, _.
+  Qed.
+
+  Section sigT_equivI.
+    Import EqNotations.
+
+    Lemma sigT_equivI {A : Type} {P : A → ofe} (x y : sigT P) :
+      x ≡ y ⊣⊢
+      ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
+    Proof.
+      apply (anti_symm _).
+      - apply (internal_eq_rewrite' x y (λ y,
+                 ∃ eq : projT1 x = projT1 y,
+                   rew eq in projT2 x ≡ projT2 y))%I;
+            [| done | exact: (exist_intro' _ _ eq_refl) ].
+        move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
+        apply exist_ne => ?. by rewrite Hab.
+      - apply exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
+        apply f_equivI, _.
+    Qed.
+  End sigT_equivI.
+
+  Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+  Proof.
+    apply (anti_symm _); auto using fun_extI.
+    apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
+  Qed.
+  Lemma ofe_morO_equivI {A B : ofe} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+  Proof.
+    apply (anti_symm _).
+    - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
+    - rewrite -(discrete_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
+      set (h1 (f : A -n> B) :=
+        exist (λ f : A -d> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
+      set (h2 (f : sigO (λ f : A -d> B, NonExpansive (f : A → B))) :=
+        @OfeMor A B (`f) (proj2_sig f)).
+      assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []).
+      assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
+      by rewrite -{2}[f]Hh -{2}[g]Hh -f_equivI -sig_equivI.
+  Qed.
+
+  Lemma pure_internal_eq {A : ofe} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y.
+  Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
+  Lemma discrete_eq {A : ofe} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝.
+  Proof.
+    intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
+  Qed.
+
+  Lemma absorbingly_internal_eq {A : ofe} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
+  Proof.
+    apply (anti_symm _), absorbingly_intro.
+    apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
+    apply wand_intro_l, internal_eq_refl.
+  Qed.
+  Lemma persistently_internal_eq {A : ofe} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
+  Proof.
+    apply (anti_symm (⊢)).
+    { by rewrite persistently_into_absorbingly absorbingly_internal_eq. }
+    apply (internal_eq_rewrite' a b (λ b, <pers> (a ≡ b))%I); auto.
+    rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
+  Qed.
+
+  Global Instance internal_eq_absorbing {A : ofe} (x y : A) :
+    Absorbing (PROP:=PROP) (x ≡ y).
+  Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
+  Global Instance internal_eq_persistent {A : ofe} (a b : A) :
+    Persistent (PROP:=PROP) (a ≡ b).
+  Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
+
+  (* Equality under a later. *)
+  Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP)
+    {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+  Proof.
+    rewrite f_equivI_contractive. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
+  Qed.
+  Lemma internal_eq_rewrite_contractive' {A : ofe} a b (Ψ : A → PROP) P
+    {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+  Proof.
+    rewrite later_equivI_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
+    by apply internal_eq_rewrite'.
+  Qed.
+
+  Lemma later_equivI {A : ofe} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
+  Proof. apply (anti_symm _); auto using later_equivI_1, later_equivI_2. Qed.
+  Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q :
+    ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
+  Proof. apply (f_equivI_contractive _). Qed.
+
+  Global Instance eq_timeless {A : ofe} (a b : A) :
+    Discrete a → Timeless (PROP:=PROP) (a ≡ b).
+  Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
 End internal_eq_derived.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 7404ef443..93d1e86b8 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -116,548 +116,548 @@ Notation "â– ? p P" := (plainly_if p P) : bi_scope.
 
 (* Derived laws *)
 Section plainly_derived.
-Context {PROP: bi} `{!BiPlainly PROP}.
-Implicit Types P : PROP.
-
-Local Hint Resolve pure_intro forall_intro : core.
-Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
-Local Hint Resolve and_intro and_elim_l' and_elim_r' : core.
-
-Global Instance plainly_proper :
-  Proper ((⊣⊢) ==> (⊣⊢)) (@plainly PROP _) := ne_proper _.
-
-Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@plainly PROP _).
-Proof. intros P Q; apply plainly_mono. Qed.
-Global Instance plainly_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
-Proof. intros P Q; apply plainly_mono. Qed.
-
-Lemma affinely_plainly_elim P : <affine> ■ P ⊢ P.
-Proof. by rewrite plainly_elim_persistently /bi_affinely persistently_and_emp_elim. Qed.
-
-Lemma persistently_elim_plainly P : <pers> ■ P ⊣⊢ ■ P.
-Proof.
-  apply (anti_symm _).
-  - by rewrite persistently_into_absorbingly /bi_absorbingly comm plainly_absorb.
-  - by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
-Qed.
-Lemma persistently_if_elim_plainly P p : <pers>?p ■ P ⊣⊢ ■ P.
-Proof. destruct p; last done. exact: persistently_elim_plainly. Qed.
-
-Lemma plainly_persistently_elim P : ■ <pers> P ⊣⊢ ■ P.
-Proof.
-  apply (anti_symm _).
-  - rewrite -{1}(left_id True%I bi_and (â–  _)%I) (plainly_emp_intro True).
-    rewrite -{2}(persistently_and_emp_elim P).
-    rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
-  - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
-Qed.
-
-Lemma absorbingly_elim_plainly P : <absorb> ■ P ⊣⊢ ■ P.
-Proof. by rewrite -(persistently_elim_plainly P) absorbingly_elim_persistently. Qed.
-
-Lemma plainly_and_sep_elim P Q : ■ P ∧ Q -∗ (emp ∧ P) ∗ Q.
-Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed.
-Lemma plainly_and_sep_assoc P Q R : ■ P ∧ (Q ∗ R) ⊣⊢ (■ P ∧ Q) ∗ R.
-Proof. by rewrite -(persistently_elim_plainly P) persistently_and_sep_assoc. Qed.
-Lemma plainly_and_emp_elim P : emp ∧ ■ P ⊢ P.
-Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
-Lemma plainly_into_absorbingly P : ■ P ⊢ <absorb> P.
-Proof. by rewrite plainly_elim_persistently persistently_into_absorbingly. Qed.
-Lemma plainly_elim P `{!Absorbing P} : ■ P ⊢ P.
-Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.
-
-Lemma plainly_idemp_1 P : ■ ■ P ⊢ ■ P.
-Proof. by rewrite plainly_into_absorbingly absorbingly_elim_plainly. Qed.
-Lemma plainly_idemp P : ■ ■ P ⊣⊢ ■ P.
-Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed.
-
-Lemma plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
-Proof. intros <-. apply plainly_idemp_2. Qed.
-
-Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢@{PROP} ⌜φ⌝.
-Proof.
-  apply (anti_symm _); auto.
-  - by rewrite plainly_elim_persistently persistently_pure.
-  - apply pure_elim'=> Hφ.
-    trans (∀ x : False, ■ True : PROP)%I; [by apply forall_intro|].
-    rewrite plainly_forall_2. by rewrite -(pure_intro φ).
-Qed.
-Lemma plainly_forall {A} (Ψ : A → PROP) : ■ (∀ a, Ψ a) ⊣⊢ ∀ a, ■ (Ψ a).
-Proof.
-  apply (anti_symm _); auto using plainly_forall_2.
-  apply forall_intro=> x. by rewrite (forall_elim x).
-Qed.
-Lemma plainly_exist_2 {A} (Ψ : A → PROP) : (∃ a, ■ (Ψ a)) ⊢ ■ (∃ a, Ψ a).
-Proof. apply exist_elim=> x. by rewrite (exist_intro x). Qed.
-Lemma plainly_exist `{!BiPlainlyExist PROP} {A} (Ψ : A → PROP) :
-  ■ (∃ a, Ψ a) ⊣⊢ ∃ a, ■ (Ψ a).
-Proof. apply (anti_symm _); auto using plainly_exist_1, plainly_exist_2. Qed.
-Lemma plainly_and P Q : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q.
-Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
-Lemma plainly_or_2 P Q : ■ P ∨ ■ Q ⊢ ■ (P ∨ Q).
-Proof. rewrite !or_alt -plainly_exist_2. by apply exist_mono=> -[]. Qed.
-Lemma plainly_or `{!BiPlainlyExist PROP} P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
-Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
-Lemma plainly_impl P Q : ■ (P → Q) ⊢ ■ P → ■ Q.
-Proof.
-  apply impl_intro_l; rewrite -plainly_and.
-  apply plainly_mono, impl_elim with P; auto.
-Qed.
-
-Lemma plainly_emp_2 : emp ⊢@{PROP} ■ emp.
-Proof. apply plainly_emp_intro. Qed.
-
-Lemma plainly_sep_dup P : ■ P ⊣⊢ ■ P ∗ ■ P.
-Proof.
-  apply (anti_symm _).
-  - rewrite -{1}(idemp bi_and (â–  _)%I).
-    by rewrite -{2}(emp_sep (â–  _)%I) plainly_and_sep_assoc and_elim_l.
-  - by rewrite plainly_absorb.
-Qed.
-
-Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
-Proof. by rewrite -{1}(emp_sep Q) plainly_and_sep_assoc and_elim_l. Qed.
-Lemma plainly_and_sep_r_1 P Q : P ∧ ■ Q ⊢ P ∗ ■ Q.
-Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
-
-Lemma plainly_True_emp : ■ True ⊣⊢@{PROP} ■ emp.
-Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
-Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊢ ■ (P ∗ Q).
-Proof.
-  rewrite plainly_and.
-  rewrite -{1}plainly_idemp -plainly_and -{1}(emp_sep Q).
-  by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
-Qed.
-
-Lemma plainly_affinely_elim P : ■ <affine> P ⊣⊢ ■ P.
-Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
-
-Lemma intuitionistically_plainly_elim P : □ ■ P -∗ □ P.
-Proof. rewrite intuitionistically_affinely plainly_elim_persistently //. Qed.
-Lemma intuitionistically_plainly P : □ ■ P -∗ ■ □ P.
-Proof.
-  rewrite /bi_intuitionistically plainly_affinely_elim affinely_elim.
-  rewrite persistently_elim_plainly plainly_persistently_elim. done.
-Qed.
-
-Lemma and_sep_plainly P Q : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q.
-Proof.
-  apply (anti_symm _); auto using plainly_and_sep_l_1.
-  apply and_intro.
-  - by rewrite plainly_absorb.
-  - by rewrite comm plainly_absorb.
-Qed.
-Lemma plainly_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
-Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
-Lemma plainly_sep `{!BiPositive PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
-Proof.
-  apply (anti_symm _); auto using plainly_sep_2.
-  rewrite -(plainly_affinely_elim (_ ∗ _)) affinely_sep -and_sep_plainly. apply and_intro.
-  - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
-  - by rewrite (affinely_elim_emp P) left_id affinely_elim.
-Qed.
-
-Lemma plainly_wand P Q : ■ (P -∗ Q) ⊢ ■ P -∗ ■ Q.
-Proof. apply wand_intro_r. by rewrite plainly_sep_2 wand_elim_l. Qed.
-
-Lemma plainly_entails_l P Q : (P ⊢ ■ Q) → P ⊢ ■ Q ∗ P.
-Proof. intros; rewrite -plainly_and_sep_l_1; auto. Qed.
-Lemma plainly_entails_r P Q : (P ⊢ ■ Q) → P ⊢ P ∗ ■ Q.
-Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed.
-
-Lemma plainly_impl_wand_2 P Q : ■ (P -∗ Q) ⊢ ■ (P → Q).
-Proof.
-  apply plainly_intro', impl_intro_r.
-  rewrite -{2}(emp_sep P) plainly_and_sep_assoc.
-  by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l.
-Qed.
-
-Lemma impl_wand_plainly_2 P Q : (■ P -∗ Q) ⊢ (■ P → Q).
-Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
-
-Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q).
-Proof. by rewrite -(persistently_elim_plainly P) impl_wand_intuitionistically. Qed.
-
-Lemma persistently_wand_affinely_plainly `{!BiPersistentlyImplPlainly PROP} P Q :
-  (<affine> ■ P -∗ <pers> Q) ⊢ <pers> (<affine> ■ P -∗ Q).
-Proof. rewrite -!impl_wand_affinely_plainly. apply: persistently_impl_plainly. Qed.
-
-Lemma plainly_wand_affinely_plainly P Q :
-  (<affine> ■ P -∗ ■ Q) ⊢ ■ (<affine> ■ P -∗ Q).
-Proof. rewrite -!impl_wand_affinely_plainly. apply plainly_impl_plainly. Qed.
-
-Section plainly_affine_bi.
-  Context `{!BiAffine PROP}.
-
-  Lemma plainly_emp : ■ emp ⊣⊢@{PROP} emp.
-  Proof. by rewrite -!True_emp plainly_pure. Qed.
-
-  Lemma plainly_and_sep_l P Q : ■ P ∧ Q ⊣⊢ ■ P ∗ Q.
+  Context {PROP: bi} `{!BiPlainly PROP}.
+  Implicit Types P : PROP.
+
+  Local Hint Resolve pure_intro forall_intro : core.
+  Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
+  Local Hint Resolve and_intro and_elim_l' and_elim_r' : core.
+
+  Global Instance plainly_proper :
+    Proper ((⊣⊢) ==> (⊣⊢)) (@plainly PROP _) := ne_proper _.
+
+  Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@plainly PROP _).
+  Proof. intros P Q; apply plainly_mono. Qed.
+  Global Instance plainly_flip_mono' :
+    Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
+  Proof. intros P Q; apply plainly_mono. Qed.
+
+  Lemma affinely_plainly_elim P : <affine> ■ P ⊢ P.
+  Proof. by rewrite plainly_elim_persistently /bi_affinely persistently_and_emp_elim. Qed.
+
+  Lemma persistently_elim_plainly P : <pers> ■ P ⊣⊢ ■ P.
+  Proof.
+    apply (anti_symm _).
+    - by rewrite persistently_into_absorbingly /bi_absorbingly comm plainly_absorb.
+    - by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
+  Qed.
+  Lemma persistently_if_elim_plainly P p : <pers>?p ■ P ⊣⊢ ■ P.
+  Proof. destruct p; last done. exact: persistently_elim_plainly. Qed.
+
+  Lemma plainly_persistently_elim P : ■ <pers> P ⊣⊢ ■ P.
+  Proof.
+    apply (anti_symm _).
+    - rewrite -{1}(left_id True%I bi_and (â–  _)%I) (plainly_emp_intro True).
+      rewrite -{2}(persistently_and_emp_elim P).
+      rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
+    - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
+  Qed.
+
+  Lemma absorbingly_elim_plainly P : <absorb> ■ P ⊣⊢ ■ P.
+  Proof. by rewrite -(persistently_elim_plainly P) absorbingly_elim_persistently. Qed.
+
+  Lemma plainly_and_sep_elim P Q : ■ P ∧ Q -∗ (emp ∧ P) ∗ Q.
+  Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed.
+  Lemma plainly_and_sep_assoc P Q R : ■ P ∧ (Q ∗ R) ⊣⊢ (■ P ∧ Q) ∗ R.
+  Proof. by rewrite -(persistently_elim_plainly P) persistently_and_sep_assoc. Qed.
+  Lemma plainly_and_emp_elim P : emp ∧ ■ P ⊢ P.
+  Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
+  Lemma plainly_into_absorbingly P : ■ P ⊢ <absorb> P.
+  Proof. by rewrite plainly_elim_persistently persistently_into_absorbingly. Qed.
+  Lemma plainly_elim P `{!Absorbing P} : ■ P ⊢ P.
+  Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.
+
+  Lemma plainly_idemp_1 P : ■ ■ P ⊢ ■ P.
+  Proof. by rewrite plainly_into_absorbingly absorbingly_elim_plainly. Qed.
+  Lemma plainly_idemp P : ■ ■ P ⊣⊢ ■ P.
+  Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed.
+
+  Lemma plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
+  Proof. intros <-. apply plainly_idemp_2. Qed.
+
+  Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢@{PROP} ⌜φ⌝.
+  Proof.
+    apply (anti_symm _); auto.
+    - by rewrite plainly_elim_persistently persistently_pure.
+    - apply pure_elim'=> Hφ.
+      trans (∀ x : False, ■ True : PROP)%I; [by apply forall_intro|].
+      rewrite plainly_forall_2. by rewrite -(pure_intro φ).
+  Qed.
+  Lemma plainly_forall {A} (Ψ : A → PROP) : ■ (∀ a, Ψ a) ⊣⊢ ∀ a, ■ (Ψ a).
+  Proof.
+    apply (anti_symm _); auto using plainly_forall_2.
+    apply forall_intro=> x. by rewrite (forall_elim x).
+  Qed.
+  Lemma plainly_exist_2 {A} (Ψ : A → PROP) : (∃ a, ■ (Ψ a)) ⊢ ■ (∃ a, Ψ a).
+  Proof. apply exist_elim=> x. by rewrite (exist_intro x). Qed.
+  Lemma plainly_exist `{!BiPlainlyExist PROP} {A} (Ψ : A → PROP) :
+    ■ (∃ a, Ψ a) ⊣⊢ ∃ a, ■ (Ψ a).
+  Proof. apply (anti_symm _); auto using plainly_exist_1, plainly_exist_2. Qed.
+  Lemma plainly_and P Q : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q.
+  Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
+  Lemma plainly_or_2 P Q : ■ P ∨ ■ Q ⊢ ■ (P ∨ Q).
+  Proof. rewrite !or_alt -plainly_exist_2. by apply exist_mono=> -[]. Qed.
+  Lemma plainly_or `{!BiPlainlyExist PROP} P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
+  Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
+  Lemma plainly_impl P Q : ■ (P → Q) ⊢ ■ P → ■ Q.
+  Proof.
+    apply impl_intro_l; rewrite -plainly_and.
+    apply plainly_mono, impl_elim with P; auto.
+  Qed.
+
+  Lemma plainly_emp_2 : emp ⊢@{PROP} ■ emp.
+  Proof. apply plainly_emp_intro. Qed.
+
+  Lemma plainly_sep_dup P : ■ P ⊣⊢ ■ P ∗ ■ P.
+  Proof.
+    apply (anti_symm _).
+    - rewrite -{1}(idemp bi_and (â–  _)%I).
+      by rewrite -{2}(emp_sep (â–  _)%I) plainly_and_sep_assoc and_elim_l.
+    - by rewrite plainly_absorb.
+  Qed.
+
+  Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
+  Proof. by rewrite -{1}(emp_sep Q) plainly_and_sep_assoc and_elim_l. Qed.
+  Lemma plainly_and_sep_r_1 P Q : P ∧ ■ Q ⊢ P ∗ ■ Q.
+  Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
+
+  Lemma plainly_True_emp : ■ True ⊣⊢@{PROP} ■ emp.
+  Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
+  Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊢ ■ (P ∗ Q).
   Proof.
-    apply (anti_symm (⊢));
-      eauto using plainly_and_sep_l_1, sep_and with typeclass_instances.
+    rewrite plainly_and.
+    rewrite -{1}plainly_idemp -plainly_and -{1}(emp_sep Q).
+    by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
   Qed.
-  Lemma plainly_and_sep_r P Q : P ∧ ■ Q ⊣⊢ P ∗ ■ Q.
-  Proof. by rewrite !(comm _ P) plainly_and_sep_l. Qed.
 
-  Lemma plainly_impl_wand P Q : ■ (P → Q) ⊣⊢ ■ (P -∗ Q).
+  Lemma plainly_affinely_elim P : ■ <affine> P ⊣⊢ ■ P.
+  Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
+
+  Lemma intuitionistically_plainly_elim P : □ ■ P -∗ □ P.
+  Proof. rewrite intuitionistically_affinely plainly_elim_persistently //. Qed.
+  Lemma intuitionistically_plainly P : □ ■ P -∗ ■ □ P.
   Proof.
-    apply (anti_symm (⊢)); auto using plainly_impl_wand_2.
-    apply plainly_intro', wand_intro_l.
-    by rewrite -plainly_and_sep_r plainly_elim impl_elim_r.
+    rewrite /bi_intuitionistically plainly_affinely_elim affinely_elim.
+    rewrite persistently_elim_plainly plainly_persistently_elim. done.
   Qed.
 
-  Lemma impl_wand_plainly P Q : (■ P → Q) ⊣⊢ (■ P -∗ Q).
+  Lemma and_sep_plainly P Q : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q.
+  Proof.
+    apply (anti_symm _); auto using plainly_and_sep_l_1.
+    apply and_intro.
+    - by rewrite plainly_absorb.
+    - by rewrite comm plainly_absorb.
+  Qed.
+  Lemma plainly_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
+  Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
+  Lemma plainly_sep `{!BiPositive PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
   Proof.
-    apply (anti_symm (⊢)).
-    - by rewrite -impl_wand_1.
-    - by rewrite impl_wand_plainly_2.
+    apply (anti_symm _); auto using plainly_sep_2.
+    rewrite -(plainly_affinely_elim (_ ∗ _)) affinely_sep -and_sep_plainly. apply and_intro.
+    - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
+    - by rewrite (affinely_elim_emp P) left_id affinely_elim.
   Qed.
-End plainly_affine_bi.
-
-(* Conditional plainly *)
-Global Instance plainly_if_ne p : NonExpansive (@plainly_if PROP _ p).
-Proof. solve_proper. Qed.
-Global Instance plainly_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@plainly_if PROP _ p).
-Proof. solve_proper. Qed.
-Global Instance plainly_if_mono' p : Proper ((⊢) ==> (⊢)) (@plainly_if PROP _ p).
-Proof. solve_proper. Qed.
-Global Instance plainly_if_flip_mono' p :
-  Proper (flip (⊢) ==> flip (⊢)) (@plainly_if PROP _ p).
-Proof. solve_proper. Qed.
-
-Lemma plainly_if_mono p P Q : (P ⊢ Q) → ■?p P ⊢ ■?p Q.
-Proof. by intros ->. Qed.
-
-Lemma plainly_if_pure p φ : ■?p ⌜φ⌝ ⊣⊢@{PROP} ⌜φ⌝.
-Proof. destruct p; simpl; auto using plainly_pure. Qed.
-Lemma plainly_if_and p P Q : ■?p (P ∧ Q) ⊣⊢ ■?p P ∧ ■?p Q.
-Proof. destruct p; simpl; auto using plainly_and. Qed.
-Lemma plainly_if_or_2 p P Q : ■?p P ∨ ■?p Q ⊢ ■?p (P ∨ Q).
-Proof. destruct p; simpl; auto using plainly_or_2. Qed.
-Lemma plainly_if_or `{!BiPlainlyExist PROP} p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
-Proof. destruct p; simpl; auto using plainly_or. Qed.
-Lemma plainly_if_exist_2 {A} p (Ψ : A → PROP) : (∃ a, ■?p (Ψ a)) ⊢ ■?p (∃ a, Ψ a).
-Proof. destruct p; simpl; auto using plainly_exist_2. Qed.
-Lemma plainly_if_exist `{!BiPlainlyExist PROP} {A} p (Ψ : A → PROP) :
-  ■?p (∃ a, Ψ a) ⊣⊢ ∃ a, ■?p (Ψ a).
-Proof. destruct p; simpl; auto using plainly_exist. Qed.
-Lemma plainly_if_sep_2 `{!BiPositive PROP} p P Q : ■?p P ∗ ■?p Q  ⊢ ■?p (P ∗ Q).
-Proof. destruct p; simpl; auto using plainly_sep_2. Qed.
-
-Lemma plainly_if_idemp p P : ■?p ■?p P ⊣⊢ ■?p P.
-Proof. destruct p; simpl; auto using plainly_idemp. Qed.
-
-(* Properties of plain propositions *)
-Global Instance Plain_proper : Proper ((≡) ==> iff) (@Plain PROP _).
-Proof. solve_proper. Qed.
-
-Lemma plain_plainly_2 P `{!Plain P} : P ⊢ ■ P.
-Proof. done. Qed.
-Lemma plain_plainly P `{!Plain P, !Absorbing P} : ■ P ⊣⊢ P.
-Proof. apply (anti_symm _), plain_plainly_2, _. by apply plainly_elim. Qed.
-Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ ■ Q.
-Proof. by intros <-. Qed.
-
-(* Typeclass instances *)
-Global Instance plainly_absorbing P : Absorbing (â–  P).
-Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorb. Qed.
-Global Instance plainly_if_absorbing P p :
-  Absorbing P → Absorbing (plainly_if p P).
-Proof. intros; destruct p; simpl; apply _. Qed.
-
-(* Not an instance, see the bottom of this file *)
-Lemma plain_persistent P : Plain P → Persistent P.
-Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
-
-Global Instance impl_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
-  Absorbing P → Plain P → Persistent Q → Persistent (P → Q).
-Proof.
-  intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
-                     -(persistent Q) (plainly_into_absorbingly P) absorbing.
-Qed.
-
-Global Instance plainly_persistent P : Persistent (â–  P).
-Proof. by rewrite /Persistent persistently_elim_plainly. Qed.
-
-Global Instance wand_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
-  Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
-Proof.
-  intros. rewrite /Persistent {2}(plain P). trans (<pers> (■ P → Q))%I.
-  - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q).
-    by rewrite affinely_plainly_elim.
-  - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
-Qed.
-
-Global Instance limit_preserving_Plain {A : ofe} `{!Cofe A} (Φ : A → PROP) :
-  NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
-Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
-
-(* Instances for big operators *)
-Global Instance plainly_sep_weak_homomorphism `{!BiPositive PROP, !BiAffine PROP} :
-  WeakMonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
-Proof. split; try apply _. apply plainly_sep. Qed.
-Global Instance plainly_sep_entails_weak_homomorphism :
-  WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
-Proof. split; try apply _. intros P Q; by rewrite plainly_sep_2. Qed.
-Global Instance plainly_sep_entails_homomorphism `{!BiAffine PROP} :
-  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
-Proof. split; try apply _. simpl. rewrite plainly_emp. done. Qed.
-
-Global Instance plainly_sep_homomorphism `{!BiAffine PROP} :
-  MonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
-Proof. split; try apply _. apply plainly_emp. Qed.
-Global Instance plainly_and_homomorphism :
-  MonoidHomomorphism bi_and bi_and (≡) (@plainly PROP _).
-Proof. split; [split|]; try apply _; [apply plainly_and | apply plainly_pure]. Qed.
-Global Instance plainly_or_homomorphism `{!BiPlainlyExist PROP} :
-  MonoidHomomorphism bi_or bi_or (≡) (@plainly PROP _).
-Proof. split; [split|]; try apply _; [apply plainly_or | apply plainly_pure]. Qed.
-
-Lemma big_sepL_plainly `{!BiAffine PROP} {A} (Φ : nat → A → PROP) l :
-  ■ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, ■ (Φ k x).
-Proof. apply (big_opL_commute _). Qed.
-Lemma big_andL_plainly {A} (Φ : nat → A → PROP) l :
-  ■ ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, ■ (Φ k x).
-Proof. apply (big_opL_commute _). Qed.
-Lemma big_orL_plainly `{!BiPlainlyExist PROP} {A} (Φ : nat → A → PROP) l :
-  ■ ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ [∨ list] k↦x ∈ l, ■ (Φ k x).
-Proof. apply (big_opL_commute _). Qed.
-
-Lemma big_sepL2_plainly `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP) l1 l2 :
-  ■ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
-  ⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, ■ (Φ k y1 y2).
-Proof. by rewrite !big_sepL2_alt plainly_and plainly_pure big_sepL_plainly. Qed.
-
-Lemma big_sepM_plainly `{!BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
-  ■ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, ■ (Φ k x).
-Proof. apply (big_opM_commute _). Qed.
-
-Lemma big_sepM2_plainly `{!BiAffine PROP, Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
-  ■ ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢ [∗ map] k↦x1;x2 ∈ m1;m2, ■ (Φ k x1 x2).
-Proof. by rewrite !big_sepM2_alt plainly_and plainly_pure big_sepM_plainly. Qed.
-
-Lemma big_sepS_plainly `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
-  ■ ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, ■ (Φ y).
-Proof. apply (big_opS_commute _). Qed.
-
-Lemma big_sepMS_plainly `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
-  ■ ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, ■ (Φ y).
-Proof. apply (big_opMS_commute _). Qed.
-
-(* Plainness instances *)
-Global Instance pure_plain φ : Plain (PROP:=PROP) ⌜φ⌝.
-Proof. by rewrite /Plain plainly_pure. Qed.
-Global Instance emp_plain : Plain (PROP:=PROP) emp.
-Proof. apply plainly_emp_intro. Qed.
-Global Instance and_plain P Q : Plain P → Plain Q → Plain (P ∧ Q).
-Proof. intros. by rewrite /Plain plainly_and -!plain. Qed.
-Global Instance or_plain P Q : Plain P → Plain Q → Plain (P ∨ Q).
-Proof. intros. by rewrite /Plain -plainly_or_2 -!plain. Qed.
-Global Instance forall_plain {A} (Ψ : A → PROP) :
-  (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x).
-Proof.
-  intros. rewrite /Plain plainly_forall. apply forall_mono=> x. by rewrite -plain.
-Qed.
-Global Instance exist_plain {A} (Ψ : A → PROP) :
-  (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x).
-Proof.
-  intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
-Qed.
-
-Global Instance impl_plain P Q : Absorbing P → Plain P → Plain Q → Plain (P → Q).
-Proof.
-  intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q)
-                     (plainly_into_absorbingly P) absorbing.
-Qed.
-Global Instance wand_plain P Q :
-  Plain P → Plain Q → Absorbing Q → Plain (P -∗ Q).
-Proof.
-  intros. rewrite /Plain {2}(plain P). trans (■ (■ P → Q))%I.
-  - rewrite -plainly_impl_plainly impl_wand_affinely_plainly -(plain Q).
-    by rewrite affinely_plainly_elim.
-  - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
-Qed.
-Global Instance sep_plain P Q : Plain P → Plain Q → Plain (P ∗ Q).
-Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
-
-Global Instance plainly_plain P : Plain (â–  P).
-Proof. by rewrite /Plain plainly_idemp. Qed.
-Global Instance persistently_plain P : Plain P → Plain (<pers> P).
-Proof.
-  rewrite /Plain=> HP. rewrite {1}HP plainly_persistently_elim persistently_elim_plainly //.
-Qed.
-Global Instance affinely_plain P : Plain P → Plain (<affine> P).
-Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance intuitionistically_plain P : Plain P → Plain (□ P).
-Proof. rewrite /bi_intuitionistically. apply _. Qed.
-Global Instance absorbingly_plain P : Plain P → Plain (<absorb> P).
-Proof. rewrite /bi_absorbingly. apply _. Qed.
-Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
-  (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
-Proof. destruct mx; apply _. Qed.
-
-Global Instance big_sepL_nil_plain `{!BiAffine PROP} {A} (Φ : nat → A → PROP) :
-  Plain ([∗ list] k↦x ∈ [], Φ k x).
-Proof. simpl; apply _. Qed.
-Global Instance big_sepL_plain `{!BiAffine PROP} {A} (Φ : nat → A → PROP) l :
-  (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x).
-Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-Global Instance big_andL_nil_plain {A} (Φ : nat → A → PROP) :
-  Plain ([∧ list] k↦x ∈ [], Φ k x).
-Proof. simpl; apply _. Qed.
-Global Instance big_andL_plain {A} (Φ : nat → A → PROP) l :
-  (∀ k x, Plain (Φ k x)) → Plain ([∧ list] k↦x ∈ l, Φ k x).
-Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-Global Instance big_orL_nil_plain {A} (Φ : nat → A → PROP) :
-  Plain ([∨ list] k↦x ∈ [], Φ k x).
-Proof. simpl; apply _. Qed.
-Global Instance big_orL_plain {A} (Φ : nat → A → PROP) l :
-  (∀ k x, Plain (Φ k x)) → Plain ([∨ list] k↦x ∈ l, Φ k x).
-Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-
-Global Instance big_sepL2_nil_plain `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP) :
-  Plain ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
-Proof. simpl; apply _. Qed.
-Global Instance big_sepL2_plain `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP) l1 l2 :
-  (∀ k x1 x2, Plain (Φ k x1 x2)) →
-  Plain ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
-Proof. rewrite big_sepL2_alt. apply _. Qed.
-
-Global Instance big_sepM_empty_plain `{!BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) :
-  Plain ([∗ map] k↦x ∈ ∅, Φ k x).
-Proof. rewrite big_opM_empty. apply _. Qed.
-Global Instance big_sepM_plain `{!BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
-  (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x ∈ m, Φ k x).
-Proof.
-  induction m using map_ind;
-    [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
-Qed.
-
-Global Instance big_sepM2_empty_plain `{!BiAffine PROP, Countable K}
-    {A B} (Φ : K → A → B → PROP) :
-  Plain ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
-Proof. rewrite big_sepM2_empty. apply _. Qed.
-Global Instance big_sepM2_plain `{!BiAffine PROP, Countable K}
-    {A B} (Φ : K → A → B → PROP) m1 m2 :
-  (∀ k x1 x2, Plain (Φ k x1 x2)) →
-  Plain ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
-Proof. intros. rewrite big_sepM2_alt. apply _. Qed.
-
-Global Instance big_sepS_empty_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) :
-  Plain ([∗ set] x ∈ ∅, Φ x).
-Proof. rewrite big_opS_empty. apply _. Qed.
-Global Instance big_sepS_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
-  (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
-Proof.
-  induction X using set_ind_L;
-    [rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
-Qed.
-Global Instance big_sepMS_empty_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) :
-  Plain ([∗ mset] x ∈ ∅, Φ x).
-Proof. rewrite big_opMS_empty. apply _. Qed.
-Global Instance big_sepMS_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
-  (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
-Proof.
-  induction X using gmultiset_ind;
-    [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
-Qed.
-
-Global Instance plainly_timeless P  `{!BiPlainlyExist PROP} :
-  Timeless P → Timeless (■ P).
-Proof.
-  intros. rewrite /Timeless /bi_except_0 later_plainly_1.
-  by rewrite (timeless P) /bi_except_0 plainly_or {1}plainly_elim.
-Qed.
-
-(* Interaction with equality *)
-Section internal_eq.
-  Context `{!BiInternalEq PROP}.
-
-  Lemma plainly_internal_eq {A:ofe} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b.
+
+  Lemma plainly_wand P Q : ■ (P -∗ Q) ⊢ ■ P -∗ ■ Q.
+  Proof. apply wand_intro_r. by rewrite plainly_sep_2 wand_elim_l. Qed.
+
+  Lemma plainly_entails_l P Q : (P ⊢ ■ Q) → P ⊢ ■ Q ∗ P.
+  Proof. intros; rewrite -plainly_and_sep_l_1; auto. Qed.
+  Lemma plainly_entails_r P Q : (P ⊢ ■ Q) → P ⊢ P ∗ ■ Q.
+  Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed.
+
+  Lemma plainly_impl_wand_2 P Q : ■ (P -∗ Q) ⊢ ■ (P → Q).
   Proof.
-    apply (anti_symm (⊢)).
-    { by rewrite plainly_elim. }
-    apply (internal_eq_rewrite' a b (λ  b, ■ (a ≡ b))%I); [solve_proper|done|].
-    rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
+    apply plainly_intro', impl_intro_r.
+    rewrite -{2}(emp_sep P) plainly_and_sep_assoc.
+    by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l.
   Qed.
 
-  Global Instance internal_eq_plain {A : ofe} (a b : A) :
-    Plain (PROP:=PROP) (a ≡ b).
-  Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
-End internal_eq.
+  Lemma impl_wand_plainly_2 P Q : (■ P -∗ Q) ⊢ (■ P → Q).
+  Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
+
+  Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q).
+  Proof. by rewrite -(persistently_elim_plainly P) impl_wand_intuitionistically. Qed.
+
+  Lemma persistently_wand_affinely_plainly `{!BiPersistentlyImplPlainly PROP} P Q :
+    (<affine> ■ P -∗ <pers> Q) ⊢ <pers> (<affine> ■ P -∗ Q).
+  Proof. rewrite -!impl_wand_affinely_plainly. apply: persistently_impl_plainly. Qed.
+
+  Lemma plainly_wand_affinely_plainly P Q :
+    (<affine> ■ P -∗ ■ Q) ⊢ ■ (<affine> ■ P -∗ Q).
+  Proof. rewrite -!impl_wand_affinely_plainly. apply plainly_impl_plainly. Qed.
+
+  Section plainly_affine_bi.
+    Context `{!BiAffine PROP}.
+
+    Lemma plainly_emp : ■ emp ⊣⊢@{PROP} emp.
+    Proof. by rewrite -!True_emp plainly_pure. Qed.
+
+    Lemma plainly_and_sep_l P Q : ■ P ∧ Q ⊣⊢ ■ P ∗ Q.
+    Proof.
+      apply (anti_symm (⊢));
+        eauto using plainly_and_sep_l_1, sep_and with typeclass_instances.
+    Qed.
+    Lemma plainly_and_sep_r P Q : P ∧ ■ Q ⊣⊢ P ∗ ■ Q.
+    Proof. by rewrite !(comm _ P) plainly_and_sep_l. Qed.
+
+    Lemma plainly_impl_wand P Q : ■ (P → Q) ⊣⊢ ■ (P -∗ Q).
+    Proof.
+      apply (anti_symm (⊢)); auto using plainly_impl_wand_2.
+      apply plainly_intro', wand_intro_l.
+      by rewrite -plainly_and_sep_r plainly_elim impl_elim_r.
+    Qed.
+
+    Lemma impl_wand_plainly P Q : (■ P → Q) ⊣⊢ (■ P -∗ Q).
+    Proof.
+      apply (anti_symm (⊢)).
+      - by rewrite -impl_wand_1.
+      - by rewrite impl_wand_plainly_2.
+    Qed.
+  End plainly_affine_bi.
+
+  (* Conditional plainly *)
+  Global Instance plainly_if_ne p : NonExpansive (@plainly_if PROP _ p).
+  Proof. solve_proper. Qed.
+  Global Instance plainly_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@plainly_if PROP _ p).
+  Proof. solve_proper. Qed.
+  Global Instance plainly_if_mono' p : Proper ((⊢) ==> (⊢)) (@plainly_if PROP _ p).
+  Proof. solve_proper. Qed.
+  Global Instance plainly_if_flip_mono' p :
+    Proper (flip (⊢) ==> flip (⊢)) (@plainly_if PROP _ p).
+  Proof. solve_proper. Qed.
+
+  Lemma plainly_if_mono p P Q : (P ⊢ Q) → ■?p P ⊢ ■?p Q.
+  Proof. by intros ->. Qed.
+
+  Lemma plainly_if_pure p φ : ■?p ⌜φ⌝ ⊣⊢@{PROP} ⌜φ⌝.
+  Proof. destruct p; simpl; auto using plainly_pure. Qed.
+  Lemma plainly_if_and p P Q : ■?p (P ∧ Q) ⊣⊢ ■?p P ∧ ■?p Q.
+  Proof. destruct p; simpl; auto using plainly_and. Qed.
+  Lemma plainly_if_or_2 p P Q : ■?p P ∨ ■?p Q ⊢ ■?p (P ∨ Q).
+  Proof. destruct p; simpl; auto using plainly_or_2. Qed.
+  Lemma plainly_if_or `{!BiPlainlyExist PROP} p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
+  Proof. destruct p; simpl; auto using plainly_or. Qed.
+  Lemma plainly_if_exist_2 {A} p (Ψ : A → PROP) : (∃ a, ■?p (Ψ a)) ⊢ ■?p (∃ a, Ψ a).
+  Proof. destruct p; simpl; auto using plainly_exist_2. Qed.
+  Lemma plainly_if_exist `{!BiPlainlyExist PROP} {A} p (Ψ : A → PROP) :
+    ■?p (∃ a, Ψ a) ⊣⊢ ∃ a, ■?p (Ψ a).
+  Proof. destruct p; simpl; auto using plainly_exist. Qed.
+  Lemma plainly_if_sep_2 `{!BiPositive PROP} p P Q : ■?p P ∗ ■?p Q  ⊢ ■?p (P ∗ Q).
+  Proof. destruct p; simpl; auto using plainly_sep_2. Qed.
+
+  Lemma plainly_if_idemp p P : ■?p ■?p P ⊣⊢ ■?p P.
+  Proof. destruct p; simpl; auto using plainly_idemp. Qed.
+
+  (* Properties of plain propositions *)
+  Global Instance Plain_proper : Proper ((≡) ==> iff) (@Plain PROP _).
+  Proof. solve_proper. Qed.
+
+  Lemma plain_plainly_2 P `{!Plain P} : P ⊢ ■ P.
+  Proof. done. Qed.
+  Lemma plain_plainly P `{!Plain P, !Absorbing P} : ■ P ⊣⊢ P.
+  Proof. apply (anti_symm _), plain_plainly_2, _. by apply plainly_elim. Qed.
+  Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ ■ Q.
+  Proof. by intros <-. Qed.
+
+  (* Typeclass instances *)
+  Global Instance plainly_absorbing P : Absorbing (â–  P).
+  Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorb. Qed.
+  Global Instance plainly_if_absorbing P p :
+    Absorbing P → Absorbing (plainly_if p P).
+  Proof. intros; destruct p; simpl; apply _. Qed.
+
+  (* Not an instance, see the bottom of this file *)
+  Lemma plain_persistent P : Plain P → Persistent P.
+  Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
+
+  Global Instance impl_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
+    Absorbing P → Plain P → Persistent Q → Persistent (P → Q).
+  Proof.
+    intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
+                       -(persistent Q) (plainly_into_absorbingly P) absorbing.
+  Qed.
 
-Section prop_ext.
-  Context `{!BiInternalEq PROP, !BiPropExt PROP}.
+  Global Instance plainly_persistent P : Persistent (â–  P).
+  Proof. by rewrite /Persistent persistently_elim_plainly. Qed.
 
-  Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
+  Global Instance wand_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
+    Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
   Proof.
-    apply (anti_symm (⊢)); last exact: prop_ext_2.
-    apply (internal_eq_rewrite' P Q (λ Q, ■ (P ∗-∗ Q))%I);
-      [ solve_proper | done | ].
-    rewrite (plainly_emp_intro (P ≡ Q)).
-    apply plainly_mono, wand_iff_refl.
+    intros. rewrite /Persistent {2}(plain P). trans (<pers> (■ P → Q))%I.
+    - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q).
+      by rewrite affinely_plainly_elim.
+    - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
   Qed.
 
-  Lemma plainly_alt P : ■ P ⊣⊢ <affine> P ≡ emp.
+  Global Instance limit_preserving_Plain {A : ofe} `{!Cofe A} (Φ : A → PROP) :
+    NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
+  Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
+
+  (* Instances for big operators *)
+  Global Instance plainly_sep_weak_homomorphism `{!BiPositive PROP, !BiAffine PROP} :
+    WeakMonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
+  Proof. split; try apply _. apply plainly_sep. Qed.
+  Global Instance plainly_sep_entails_weak_homomorphism :
+    WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
+  Proof. split; try apply _. intros P Q; by rewrite plainly_sep_2. Qed.
+  Global Instance plainly_sep_entails_homomorphism `{!BiAffine PROP} :
+    MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
+  Proof. split; try apply _. simpl. rewrite plainly_emp. done. Qed.
+
+  Global Instance plainly_sep_homomorphism `{!BiAffine PROP} :
+    MonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
+  Proof. split; try apply _. apply plainly_emp. Qed.
+  Global Instance plainly_and_homomorphism :
+    MonoidHomomorphism bi_and bi_and (≡) (@plainly PROP _).
+  Proof. split; [split|]; try apply _; [apply plainly_and | apply plainly_pure]. Qed.
+  Global Instance plainly_or_homomorphism `{!BiPlainlyExist PROP} :
+    MonoidHomomorphism bi_or bi_or (≡) (@plainly PROP _).
+  Proof. split; [split|]; try apply _; [apply plainly_or | apply plainly_pure]. Qed.
+
+  Lemma big_sepL_plainly `{!BiAffine PROP} {A} (Φ : nat → A → PROP) l :
+    ■ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, ■ (Φ k x).
+  Proof. apply (big_opL_commute _). Qed.
+  Lemma big_andL_plainly {A} (Φ : nat → A → PROP) l :
+    ■ ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, ■ (Φ k x).
+  Proof. apply (big_opL_commute _). Qed.
+  Lemma big_orL_plainly `{!BiPlainlyExist PROP} {A} (Φ : nat → A → PROP) l :
+    ■ ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ [∨ list] k↦x ∈ l, ■ (Φ k x).
+  Proof. apply (big_opL_commute _). Qed.
+
+  Lemma big_sepL2_plainly `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP) l1 l2 :
+    ■ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
+    ⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, ■ (Φ k y1 y2).
+  Proof. by rewrite !big_sepL2_alt plainly_and plainly_pure big_sepL_plainly. Qed.
+
+  Lemma big_sepM_plainly `{!BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
+    ■ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, ■ (Φ k x).
+  Proof. apply (big_opM_commute _). Qed.
+
+  Lemma big_sepM2_plainly `{!BiAffine PROP, Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
+    ■ ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢ [∗ map] k↦x1;x2 ∈ m1;m2, ■ (Φ k x1 x2).
+  Proof. by rewrite !big_sepM2_alt plainly_and plainly_pure big_sepM_plainly. Qed.
+
+  Lemma big_sepS_plainly `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
+    ■ ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, ■ (Φ y).
+  Proof. apply (big_opS_commute _). Qed.
+
+  Lemma big_sepMS_plainly `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
+    ■ ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, ■ (Φ y).
+  Proof. apply (big_opMS_commute _). Qed.
+
+  (* Plainness instances *)
+  Global Instance pure_plain φ : Plain (PROP:=PROP) ⌜φ⌝.
+  Proof. by rewrite /Plain plainly_pure. Qed.
+  Global Instance emp_plain : Plain (PROP:=PROP) emp.
+  Proof. apply plainly_emp_intro. Qed.
+  Global Instance and_plain P Q : Plain P → Plain Q → Plain (P ∧ Q).
+  Proof. intros. by rewrite /Plain plainly_and -!plain. Qed.
+  Global Instance or_plain P Q : Plain P → Plain Q → Plain (P ∨ Q).
+  Proof. intros. by rewrite /Plain -plainly_or_2 -!plain. Qed.
+  Global Instance forall_plain {A} (Ψ : A → PROP) :
+    (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x).
   Proof.
-    rewrite -plainly_affinely_elim. apply (anti_symm (⊢)).
-    - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
-      + by rewrite affinely_elim_emp left_id.
-      + by rewrite left_id.
-    - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
-      by rewrite -plainly_True_emp plainly_pure True_impl.
+    intros. rewrite /Plain plainly_forall. apply forall_mono=> x. by rewrite -plain.
+  Qed.
+  Global Instance exist_plain {A} (Ψ : A → PROP) :
+    (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x).
+  Proof.
+    intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
   Qed.
 
-  Lemma plainly_alt_absorbing P `{!Absorbing P} : ■ P ⊣⊢ P ≡ True.
+  Global Instance impl_plain P Q : Absorbing P → Plain P → Plain Q → Plain (P → Q).
+  Proof.
+    intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q)
+                       (plainly_into_absorbingly P) absorbing.
+  Qed.
+  Global Instance wand_plain P Q :
+    Plain P → Plain Q → Absorbing Q → Plain (P -∗ Q).
+  Proof.
+    intros. rewrite /Plain {2}(plain P). trans (■ (■ P → Q))%I.
+    - rewrite -plainly_impl_plainly impl_wand_affinely_plainly -(plain Q).
+      by rewrite affinely_plainly_elim.
+    - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
+  Qed.
+  Global Instance sep_plain P Q : Plain P → Plain Q → Plain (P ∗ Q).
+  Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
+
+  Global Instance plainly_plain P : Plain (â–  P).
+  Proof. by rewrite /Plain plainly_idemp. Qed.
+  Global Instance persistently_plain P : Plain P → Plain (<pers> P).
+  Proof.
+    rewrite /Plain=> HP. rewrite {1}HP plainly_persistently_elim persistently_elim_plainly //.
+  Qed.
+  Global Instance affinely_plain P : Plain P → Plain (<affine> P).
+  Proof. rewrite /bi_affinely. apply _. Qed.
+  Global Instance intuitionistically_plain P : Plain P → Plain (□ P).
+  Proof. rewrite /bi_intuitionistically. apply _. Qed.
+  Global Instance absorbingly_plain P : Plain P → Plain (<absorb> P).
+  Proof. rewrite /bi_absorbingly. apply _. Qed.
+  Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
+    (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
+  Proof. destruct mx; apply _. Qed.
+
+  Global Instance big_sepL_nil_plain `{!BiAffine PROP} {A} (Φ : nat → A → PROP) :
+    Plain ([∗ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL_plain `{!BiAffine PROP} {A} (Φ : nat → A → PROP) l :
+    (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x).
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Global Instance big_andL_nil_plain {A} (Φ : nat → A → PROP) :
+    Plain ([∧ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_andL_plain {A} (Φ : nat → A → PROP) l :
+    (∀ k x, Plain (Φ k x)) → Plain ([∧ list] k↦x ∈ l, Φ k x).
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Global Instance big_orL_nil_plain {A} (Φ : nat → A → PROP) :
+    Plain ([∨ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_orL_plain {A} (Φ : nat → A → PROP) l :
+    (∀ k x, Plain (Φ k x)) → Plain ([∨ list] k↦x ∈ l, Φ k x).
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
+  Global Instance big_sepL2_nil_plain `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP) :
+    Plain ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL2_plain `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP) l1 l2 :
+    (∀ k x1 x2, Plain (Φ k x1 x2)) →
+    Plain ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+  Proof. rewrite big_sepL2_alt. apply _. Qed.
+
+  Global Instance big_sepM_empty_plain `{!BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) :
+    Plain ([∗ map] k↦x ∈ ∅, Φ k x).
+  Proof. rewrite big_opM_empty. apply _. Qed.
+  Global Instance big_sepM_plain `{!BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
+    (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x ∈ m, Φ k x).
+  Proof.
+    induction m using map_ind;
+      [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
+  Qed.
+
+  Global Instance big_sepM2_empty_plain `{!BiAffine PROP, Countable K}
+      {A B} (Φ : K → A → B → PROP) :
+    Plain ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
+  Proof. rewrite big_sepM2_empty. apply _. Qed.
+  Global Instance big_sepM2_plain `{!BiAffine PROP, Countable K}
+      {A B} (Φ : K → A → B → PROP) m1 m2 :
+    (∀ k x1 x2, Plain (Φ k x1 x2)) →
+    Plain ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
+  Proof. intros. rewrite big_sepM2_alt. apply _. Qed.
+
+  Global Instance big_sepS_empty_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) :
+    Plain ([∗ set] x ∈ ∅, Φ x).
+  Proof. rewrite big_opS_empty. apply _. Qed.
+  Global Instance big_sepS_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
+    (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
+  Proof.
+    induction X using set_ind_L;
+      [rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
+  Qed.
+  Global Instance big_sepMS_empty_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) :
+    Plain ([∗ mset] x ∈ ∅, Φ x).
+  Proof. rewrite big_opMS_empty. apply _. Qed.
+  Global Instance big_sepMS_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
+    (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
   Proof.
-    apply (anti_symm (⊢)).
-    - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
-    - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
-      by rewrite plainly_pure True_impl.
+    induction X using gmultiset_ind;
+      [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
   Qed.
 
-  Lemma plainly_True_alt P : ■ (True -∗ P) ⊣⊢ P ≡ True.
+  Global Instance plainly_timeless P  `{!BiPlainlyExist PROP} :
+    Timeless P → Timeless (■ P).
   Proof.
-    apply (anti_symm (⊢)).
-    - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
-      by rewrite wand_elim_r.
-    - rewrite internal_eq_sym (internal_eq_rewrite _ _
-        (λ Q, ■ (True -∗ Q))%I ltac:(shelve)); last solve_proper.
-      by rewrite -entails_wand // -(plainly_emp_intro True) True_impl.
+    intros. rewrite /Timeless /bi_except_0 later_plainly_1.
+    by rewrite (timeless P) /bi_except_0 plainly_or {1}plainly_elim.
   Qed.
 
-  (* This proof uses [BiPlainlyExist] and [BiLöb] via [plainly_timeless] and
-  [wand_timeless]. *)
-  Global Instance internal_eq_timeless `{!BiPlainlyExist PROP, !BiLöb PROP}
-      `{!Timeless P} `{!Timeless Q} :
-    Timeless (PROP := PROP) (P ≡ Q).
-  Proof. rewrite prop_ext. apply _. Qed.
-End prop_ext.
-
-(* Interaction with â–· *)
-Lemma later_plainly P : ▷ ■ P ⊣⊢ ■ ▷ P.
-Proof. apply (anti_symm _); auto using later_plainly_1, later_plainly_2. Qed.
-Lemma laterN_plainly n P : ▷^n ■ P ⊣⊢ ■ ▷^n P.
-Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_plainly. Qed.
-
-Lemma later_plainly_if p P : ▷ ■?p P ⊣⊢ ■?p ▷ P.
-Proof. destruct p; simpl; auto using later_plainly. Qed.
-Lemma laterN_plainly_if n p P : ▷^n ■?p P ⊣⊢ ■?p (▷^n P).
-Proof. destruct p; simpl; auto using laterN_plainly. Qed.
-
-Lemma except_0_plainly_1 P : ◇ ■ P ⊢ ■ ◇ P.
-Proof. by rewrite /bi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
-Lemma except_0_plainly `{!BiPlainlyExist PROP} P : ◇ ■ P ⊣⊢ ■ ◇ P.
-Proof. by rewrite /bi_except_0 plainly_or -later_plainly plainly_pure. Qed.
-
-Global Instance later_plain P : Plain P → Plain (▷ P).
-Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed.
-Global Instance laterN_plain n P : Plain P → Plain (▷^n P).
-Proof. induction n; apply _. Qed.
-Global Instance except_0_plain P : Plain P → Plain (◇ P).
-Proof. rewrite /bi_except_0; apply _. Qed.
+  (* Interaction with equality *)
+  Section internal_eq.
+    Context `{!BiInternalEq PROP}.
+
+    Lemma plainly_internal_eq {A:ofe} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b.
+    Proof.
+      apply (anti_symm (⊢)).
+      { by rewrite plainly_elim. }
+      apply (internal_eq_rewrite' a b (λ  b, ■ (a ≡ b))%I); [solve_proper|done|].
+      rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
+    Qed.
+
+    Global Instance internal_eq_plain {A : ofe} (a b : A) :
+      Plain (PROP:=PROP) (a ≡ b).
+    Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
+  End internal_eq.
+
+  Section prop_ext.
+    Context `{!BiInternalEq PROP, !BiPropExt PROP}.
+
+    Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
+    Proof.
+      apply (anti_symm (⊢)); last exact: prop_ext_2.
+      apply (internal_eq_rewrite' P Q (λ Q, ■ (P ∗-∗ Q))%I);
+        [ solve_proper | done | ].
+      rewrite (plainly_emp_intro (P ≡ Q)).
+      apply plainly_mono, wand_iff_refl.
+    Qed.
+
+    Lemma plainly_alt P : ■ P ⊣⊢ <affine> P ≡ emp.
+    Proof.
+      rewrite -plainly_affinely_elim. apply (anti_symm (⊢)).
+      - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
+        + by rewrite affinely_elim_emp left_id.
+        + by rewrite left_id.
+      - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
+        by rewrite -plainly_True_emp plainly_pure True_impl.
+    Qed.
+
+    Lemma plainly_alt_absorbing P `{!Absorbing P} : ■ P ⊣⊢ P ≡ True.
+    Proof.
+      apply (anti_symm (⊢)).
+      - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+      - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
+        by rewrite plainly_pure True_impl.
+    Qed.
+
+    Lemma plainly_True_alt P : ■ (True -∗ P) ⊣⊢ P ≡ True.
+    Proof.
+      apply (anti_symm (⊢)).
+      - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+        by rewrite wand_elim_r.
+      - rewrite internal_eq_sym (internal_eq_rewrite _ _
+          (λ Q, ■ (True -∗ Q))%I ltac:(shelve)); last solve_proper.
+        by rewrite -entails_wand // -(plainly_emp_intro True) True_impl.
+    Qed.
+
+    (* This proof uses [BiPlainlyExist] and [BiLöb] via [plainly_timeless] and
+    [wand_timeless]. *)
+    Global Instance internal_eq_timeless `{!BiPlainlyExist PROP, !BiLöb PROP}
+        `{!Timeless P} `{!Timeless Q} :
+      Timeless (PROP := PROP) (P ≡ Q).
+    Proof. rewrite prop_ext. apply _. Qed.
+  End prop_ext.
+
+  (* Interaction with â–· *)
+  Lemma later_plainly P : ▷ ■ P ⊣⊢ ■ ▷ P.
+  Proof. apply (anti_symm _); auto using later_plainly_1, later_plainly_2. Qed.
+  Lemma laterN_plainly n P : ▷^n ■ P ⊣⊢ ■ ▷^n P.
+  Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_plainly. Qed.
+
+  Lemma later_plainly_if p P : ▷ ■?p P ⊣⊢ ■?p ▷ P.
+  Proof. destruct p; simpl; auto using later_plainly. Qed.
+  Lemma laterN_plainly_if n p P : ▷^n ■?p P ⊣⊢ ■?p (▷^n P).
+  Proof. destruct p; simpl; auto using laterN_plainly. Qed.
+
+  Lemma except_0_plainly_1 P : ◇ ■ P ⊢ ■ ◇ P.
+  Proof. by rewrite /bi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
+  Lemma except_0_plainly `{!BiPlainlyExist PROP} P : ◇ ■ P ⊣⊢ ■ ◇ P.
+  Proof. by rewrite /bi_except_0 plainly_or -later_plainly plainly_pure. Qed.
+
+  Global Instance later_plain P : Plain P → Plain (▷ P).
+  Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed.
+  Global Instance laterN_plain n P : Plain P → Plain (▷^n P).
+  Proof. induction n; apply _. Qed.
+  Global Instance except_0_plain P : Plain P → Plain (◇ P).
+  Proof. rewrite /bi_except_0; apply _. Qed.
 
 End plainly_derived.
 
-- 
GitLab