Shorten proof.

theories/base_logic/derived.v

@@ -981,13 +981,9 @@ Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
 Lemma plainly_alt P : ■ P ⊣⊢ P ≡ True.
 Proof.
   apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_intro'. rewrite plainly_elim.
-    apply and_intro; apply impl_intro_r.
-    + apply True_intro.
-    + apply and_elim_l.
+  - rewrite -prop_ext. apply plainly_mono, and_intro; apply impl_intro_r; auto.
   - rewrite internal_eq_sym (internal_eq_rewrite _ _ (λ P, ■ P)%I).
-    eapply impl_elim; first reflexivity.
-    rewrite plainly_pure. apply True_intro.
+    by rewrite plainly_pure True_impl.
 Qed.
 
 Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.