diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index f8b24ad03ce1542d00f4b11e8bf1f25a0a0164fd..55f213448edb758142cd0a5ed2cd38267a548e6a 100644
--- a/theories/base_logic/derived.v
+++ b/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.