Remove admissable rule for `plainly`.

theories/base_logic/upred.v

@@ -486,8 +486,6 @@ Proof.
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
   - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
     intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
-  - (* bi_plainly (bi_persistently P) ⊢ bi_plainly P (ADMISSIBLE) *)
-    intros P. unseal; split=> n  x ?? /=. by rewrite -(core_id_core ε).
   - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
     by unseal.
   - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)

theories/bi/derived_laws.v

@@ -957,8 +957,11 @@ Proof.
 Qed.
 Lemma plainly_persistently P : bi_plainly (bi_persistently P) ⊣⊢ bi_plainly P.
 Proof.
-  apply (anti_symm _); first apply plainly_persistently_1.
-  by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
+  apply (anti_symm _).
+  - rewrite -{1}(left_id True%I bi_and (bi_plainly _)) (plainly_emp_intro True%I).
+    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_plainly P : bi_absorbingly (bi_plainly P) ⊣⊢ bi_plainly P.

theories/bi/interface.v

@@ -129,8 +129,6 @@ Section bi_mixin.
     (* In the ordered RA model: `core` is idempotent *)
     bi_mixin_persistently_idemp_2 P :
       bi_persistently P ⊢ bi_persistently (bi_persistently P);
-    bi_mixin_plainly_persistently_1 P :
-      bi_plainly (bi_persistently P) ⊢ bi_plainly P;
 
     (* In the ordered RA model [P ⊢ persisently emp] (which can currently still
     be derived from the plainly axioms, which will be removed): `ε ≼ core x` *)
@@ -453,9 +451,6 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
 Lemma persistently_idemp_2 P :
   bi_persistently P ⊢ bi_persistently (bi_persistently P).
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
-Lemma plainly_persistently_1 P :
-  bi_plainly (bi_persistently P) ⊢ bi_plainly P.
-Proof. eapply (bi_mixin_plainly_persistently_1 bi_entails), bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
   (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).

theories/bi/monpred.v

@@ -326,7 +326,6 @@ Proof.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.
   - intros P Q [?]. split=> i /=. by f_equiv.
   - intros P. split=> i. by apply bi.persistently_idemp_2.
-  - intros P. split=> i /=. by setoid_rewrite bi.plainly_persistently_1.
   - intros A Ψ. split=> i. by apply bi.persistently_forall_2.
   - intros A Ψ. split=> i. by apply bi.persistently_exist_1.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.