From 016cd8208557c753609704d1ac893637ab29f1b7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 May 2020 16:56:45 +0200
Subject: [PATCH] =?UTF-8?q?Simplify=20proof=20of=20`tac=5Fl=C3=B6b`=20usin?=
 =?UTF-8?q?g=20new=20lemma=20`l=C3=B6b=5Fwand=5Fintuitionistically`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/coq_tactics.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 7a90a32fd..3bc66cbd1 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -844,11 +844,8 @@ Proof.
   destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
   rewrite envs_entails_eq => ?? HQ.
   rewrite (env_spatial_is_nil_intuitionistically Δ) //.
-  rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
-  rewrite -(löb (<pers> Q)%I) later_persistently. apply impl_intro_l.
-  rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
-  rewrite persistently_and_intuitionistically_sep_l -{1}intuitionistically_idemp.
-  rewrite intuitionistically_sep_2 wand_elim_r intuitionistically_into_persistently_1 //.
+  rewrite envs_app_singleton_sound //; simpl. rewrite HQ.
+  apply löb_wand_intuitionistically.
 Qed.
 End tactics.
 
-- 
GitLab