diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 7b8a79d49fc874cc604a195e0627b505666f6bbe..f3e5d9502ab5146563481ca229c9e6552bfd8ff5 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -123,11 +123,7 @@ Proof.
     + rewrite -EQ impl_elim_r. done.
 Qed.
 Lemma entails_impl_True P Q : (P ⊢ Q) ↔ (True ⊢ (P → Q)).
-Proof.
-  rewrite entails_eq_True. split.
-  - by intros <-.
-  - intros. apply (anti_symm (⊢)); last done. apply True_intro.
-Qed.
+Proof. rewrite entails_eq_True equiv_spec; naive_solver. Qed.
 
 Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
 Proof. auto. Qed.