diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 22b2f301d7ca2b517816f6dc09872b9b2a61e1b8..e48d0aea8b2441cd7d644855dafad47e27c3e294 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).