diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 12110588e7cc5a2d5c0869457d8230754ed043d2..e5ae5ee4f6f953afbcb58cf870b44fdff360f5f2 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -63,7 +63,6 @@ Section typing.
         ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
           (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
             elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
-            elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
   Global Arguments typed_write _%EL _%LL _%T _%T _%T.
 
   (* Technically speaking, we could remvoe the vl quantifiaction here and use