From c4f2d1ee00113380e7ab55aab270a56246c8f0e7 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 22 Mar 2017 14:55:04 +0100
Subject: [PATCH] WIP.

---
 theories/typing/sum.v | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 22b2f301..e48d0aea 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -183,12 +183,10 @@ Section sum.
   Lemma emp_sum E L :
     eqtype E L emp (sum []).
   Proof.
-    split; (iIntros (q) "_ _"; iSplit; first done; iSplit; iAlways).
-    - iIntros (??) "[]".
-    - iIntros (κ tid l) "[]".
-    - iIntros (??) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
-      by rewrite nth_empty.
-    - iIntros (???) "H". iDestruct "H" as (i) "(_ & Hshr)". by rewrite nth_empty.
+    apply eqtype_unfold. iIntros (?) "_ !# _".
+    iSplit; first done; iSplit; iAlways; iIntros; iSplit; try by iIntros "[]".
+    - iIntros "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)". by rewrite nth_empty.
+    - iIntros "H". iDestruct "H" as (i) "(_ & Hshr)". by rewrite nth_empty.
   Qed.
 
   Global Instance sum_copy tyl : LstCopy tyl → Copy (sum tyl).
-- 
GitLab