Shorten proof.

bdb566a4 · Robbert Krebbers · e4091905 · bdb566a4
Commit bdb566a4 authored May 07, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 5 deletions

theories/bi/derived_laws_bi.v theories/bi/derived_laws_bi.v +1 -5

No files found.
--- 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.