From 4f15337d5b5fed20a3cff4a65f9c3b64f158a338 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 9 Sep 2016 14:31:41 +0200
Subject: [PATCH] More simplifications
---
types.v | 11 +++++------
1 file changed, 5 insertions(+), 6 deletions(-)
diff --git a/types.v b/types.v
index d56bc0a5..875b82d7 100644
--- a/types.v
+++ b/types.v
@@ -386,12 +386,11 @@ Section types.
{ intros. rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
instantiate (1:=λ _ y, _). simpl. reflexivity. }
rewrite big_sepL_sepL. iDestruct "Hownq" as "[Hownq0 Hownq1]".
- iSplitR "Hcloseq Hcloseh Hownh1 Hownq1".
- + iNext. by iFrame.
- + iIntros "[Hh Hq]". rewrite (lft_own_split κ q).
- iVs ("Hcloseh" with "[Hh Hownh1]") as "($&$)". iNext. by iFrame.
- iVs ("Hcloseq" with "[Hq Hownq1]") as "($&$&$)". iNext. by iFrame.
- done.
+ iSplitL "Hownh0 Hownq0". iNext. by iFrame.
+ iIntros "[Hh Hq]". rewrite (lft_own_split κ q).
+ iVs ("Hcloseh" with "[Hh Hownh1]") as "($&$)". iNext. by iFrame.
+ iVs ("Hcloseq" with "[Hq Hownq1]") as "($&$&$)". iNext. by iFrame.
+ done.
Qed.
End types.
--
GitLab