diff --git a/_CoqProject b/_CoqProject
index 40ecd9a46c6484165bc734b27892b8c2d797a354..6f953fda74213e58bc9ba18c7a5410584c446712 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -41,4 +41,4 @@ theories/typing/programs.v
 theories/typing/borrow.v
 theories/typing/cont.v
 theories/typing/fixpoint.v
-theories/typing/case.v
+theories/typing/type_sum.v
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index 59c8c1178f9d804ccafe971ac863a1a12677cdb5..e65919f1c88aa0815726d06d95d72d67bdf6164a 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -9,22 +9,22 @@ Definition memcpy : val :=
          "memcpy" ["dst" +â‚— #1 ; "len" - #1 ; "src" +â‚— #1].
 Global Opaque memcpy.
 
-Notation "e1 <-{ n } ! e2" :=
+Notation "e1 <⋯ !{ n } e2" :=
   (memcpy (@cons expr e1%E
           (@cons expr (Lit n)
           (@cons expr e2%E nil))))
-  (at level 80, n at next level, format "e1  <-{ n }  ! e2") : expr_scope.
+  (at level 80, n at next level, format "e1  <⋯  !{ n } e2") : expr_scope.
 
-Notation "e1 <-[ i ]{ n } ! e2" :=
-  (e1 <-[i] ☇ ;; e1+ₗ#1 <-{n} !e2)%E
+Notation "e1 <⋯{ i } !{ n } e2" :=
+  (e1 <-{i} ☇ ;; e1+ₗ#1 <⋯ !{n}e2)%E
   (at level 80, n, i at next level,
-   format "e1  <-[ i ]{ n }  ! e2") : lrust_expr_scope.
+   format "e1  <⋯{ i }  !{ n } e2") : expr_scope.
 
 Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
   ↑heapN ⊆ E →
   length vl1 = n → length vl2 = n →
   {{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
-    #l1 <-{n} !#l2 @ E
+    #l1 <⋯ !{n}#l2 @ E
   {{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
 Proof.
   iIntros (? Hvl1 Hvl2 Φ) "(#Hinv & Hl1 & Hl2) HΦ".
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index 6318799bafe2139799079d093c3902f3d8aadbe1..5c6c407c6ec2a980c0887d089c14d8ffda92bb0d 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -45,5 +45,5 @@ Notation "'letalloc:' x := e1 'in' e2" :=
   ((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
 Notation "'letalloc:' x :={ n } ! e1 'in' e2" :=
-  ((Lam (@cons binder x%E%E%E nil) (x <-{ n%Z%V } ! e1 ;; e2)) [new [ #n]%E%E])%E
+  ((Lam (@cons binder x%E%E%E nil) (x <⋯ !{n%Z%V}e1 ;; e2)) [new [ #n]%E%E])%E
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 176b7adbe63f949fde5dc44281e43d1681d85f9e..86ab9ab4e6d5da7ddba3c2af29bb68b189d86ffd 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -79,7 +79,7 @@ Notation "'letcall:' x := f args 'in' e" :=
   (letcont: "_k" [ x ] := e in call: f args → "_k")%E
   (at level 102, x, f, args at level 1, e at level 200) : expr_scope.
 
-Notation "e1 <-[ i ] '☇'" := (e1 <- #i)%E
+Notation "e1 <-{ i } '☇'" := (e1 <- #i)%E
   (only parsing, at level 80) : expr_scope.
-Notation "e1 <-[ i ] e2" := (e1 <-[i] ☇ ;; e1+ₗ#1 <- e2)%E
+Notation "e1 <-{ i } e2" := (e1 <-{i} ☇ ;; e1+ₗ#1 <- e2)%E
   (at level 80) : expr_scope.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 256d7b41d5f31c77438ca25a399301822bfe9ffa..8b1f5bc8c218960222d5baec9d276234b9d96f86 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -63,7 +63,7 @@ Section own.
     move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
     iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
     iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver. 
+    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
     iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
     iMod (bor_persistent_tok with "LFT EQ Htok") as "[>% $]". set_solver.
     iExists l'. subst. rewrite heap_mapsto_vec_singleton.
@@ -256,8 +256,8 @@ Section typing.
     - apply type_new.
     - solve_typing.
     - move=>xv /=.
-      assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
-              (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
+      assert (subst x xv (x <⋯ !{ty.(ty_size)}p ;; e)%E =
+              (xv <⋯ !{ty.(ty_size)}p ;; subst x xv e)%E) as ->.
       { (* TODO : simpl_subst should be able to do this. *)
         unfold subst=>/=. repeat f_equal.
         - eapply (is_closed_subst []). done. set_solver.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 5ce9ce92619a3507fcce9b3a119dd0c37894b83a..bc05db76b95aa50da3bf5e1a985a6a783abb5e8e 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -177,7 +177,7 @@ Section typing_rules.
     ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
     {{{ heap_ctx ∗ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
         tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
-      (p1 <-{n} !p2)
+      (p1 <⋯ !{n}p2)
     {{{ RET #(); na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
                  tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
@@ -199,7 +199,7 @@ Section typing_rules.
 
   Lemma type_memcpy {E L} ty ty1 ty1' ty2 ty2' n p1 p2 :
     ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <⋯ !{n}p2)
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
     iIntros (Hsz Hwrt Hread tid qE) "#HEAP #LFT Htl HE HL HT".
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 33596b8e419f8ea05f8fa68ec9b628110936e70c..258f75723f34324c18ee51a2324a35633c51bd2a 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -63,6 +63,16 @@ Section type_context.
     iIntros (v) "%". subst v. wp_op. done.
   Qed.
 
+  Lemma eval_path_closed p v :
+    eval_path p = Some v → Closed [] p.
+  Proof.
+    intros Hpv. revert v Hpv.
+    induction p as [| | |[] p IH [|[]| | | | | | | | | |] _| | | | | | | |]=>//.
+    - unfold eval_path=>? /of_to_val <-. apply is_closed_of_val.
+    - simpl. destruct (eval_path p) as [[[]|]|]; intros ? [= <-].
+      specialize (IH _ eq_refl). apply _.
+  Qed.
+
   (** Type context element *)
   Definition tctx_elt_interp (tid : thread_id) (x : tctx_elt) : iProp Σ :=
     match x with
@@ -106,6 +116,11 @@ Section type_context.
     iIntros (v') "%". subst v'. iApply ("HΦ" with "* [] Hown"). by auto.
   Qed.
 
+  Lemma closed_hasty tid p ty : tctx_elt_interp tid (p ◁ ty) -∗ ⌜Closed [] p⌝.
+  Proof.
+    iIntros "H". iDestruct "H" as (?) "[% _]". eauto using eval_path_closed.
+  Qed.
+
   (** Type context *)
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
     ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
diff --git a/theories/typing/case.v b/theories/typing/type_sum.v
similarity index 64%
rename from theories/typing/case.v
rename to theories/typing/type_sum.v
index 99bb0d84c7db1ec9f3518381cac0a2437df3e8c2..8276d880ccd31e2bac580063f0719f3af9f22c18 100644
--- a/theories/typing/case.v
+++ b/theories/typing/type_sum.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
-From lrust.lang Require Import heap.
+From lrust.lang Require Import heap memcpy.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export uninit uniq_bor shr_bor own sum.
-From lrust.typing Require Import lft_contexts type_context programs.
+From lrust.typing Require Import lft_contexts type_context programs product.
 
 Section case.
   Context `{typeG Σ}.
@@ -151,4 +151,84 @@ Section case.
     intros. rewrite ->copy_elem_of_tctx_incl; last done; last apply _.
     apply type_case_shr; first done. eapply Forall2_impl; first done. auto.
   Qed.
+
+  Lemma type_sum_assign {E L} (i : nat) tyl ty1 ty2 ty p1 p2 :
+    Closed [] p1 → Closed [] p2 →
+    tyl !! i = Some ty →
+    typed_write E L ty1 (sum tyl) ty2 →
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{i} p2) (λ _, [p1 ◁ ty2]%TC).
+  Proof.
+    iIntros (?? Hty Hw ??) "#HEAP #LFT $ HE HL Hp".
+    rewrite tctx_interp_cons tctx_interp_singleton.
+    iDestruct "Hp" as "[Hp1 Hp2]". wp_bind p1. iApply (wp_hasty with "Hp1").
+    iIntros (v1 Hv1) "Hty1".
+    iMod (Hw with "LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
+    destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
+    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
+    wp_write. iApply wp_seq. done. iNext. wp_bind p1.
+    iApply (wp_wand with "[]"); first by iApply (wp_eval_path).
+    iIntros (? ->). wp_op. wp_bind p2. iApply (wp_hasty with "Hp2").
+    iIntros (v2 Hv2) "Hty2". iDestruct (ty_size_eq with "Hty2") as %Hlenty.
+    destruct vl as [|? vl].
+    { exfalso. revert i Hty. clear - Hlen Hlenty. induction tyl=>//= -[|i] /=.
+      - intros [= ->]. simpl in *. lia.
+      - apply IHtyl. simpl in *. lia. }
+    rewrite heap_mapsto_vec_cons. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
+    rewrite tctx_interp_singleton tctx_hasty_val' //. iApply "Hw". iNext.
+    iExists (_::_::_). rewrite !heap_mapsto_vec_cons. iFrame.
+    iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
+  Qed.
+
+  Lemma type_sum_assign_unit {E L} (i : nat) tyl ty1 ty2 p :
+    tyl !! i = Some unit →
+    typed_write E L ty1 (sum tyl) ty2 →
+    typed_instruction E L [p ◁ ty1] (p <-{i} ☇) (λ _, [p ◁ ty2]%TC).
+  Proof.
+    iIntros (Hty Hw ??) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
+    iMod (Hw with "LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
+    simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
+    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
+    wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
+    iApply "Hw". iModIntro. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
+    iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
+  Qed.
+
+  Lemma type_sum_memcpy {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
+    Closed [] p1 → Closed [] p2 →
+    tyl !! i = Some ty →
+    typed_write E L ty1 (sum tyl) ty1' →
+    typed_read E L ty2 ty ty2' →
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
+               (p1 <⋯{i} !{ty.(ty_size)}p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
+  Proof.
+    iIntros (?? Hty Hw Hr ??) "#HEAP #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
+    rewrite tctx_interp_cons tctx_interp_singleton.
+    iDestruct "Hp" as "[Hp1 Hp2]". wp_bind p1. iApply (wp_hasty with "Hp1").
+    iIntros (v1 Hv1) "Hty1".
+    iMod (Hw with "LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
+    destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
+    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
+    iApply wp_seq. done. iNext. wp_bind p1.
+    iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
+    wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
+    iMod (Hr with "LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=. subst.
+    assert (ty.(ty_size) ≤ length vl1).
+    { revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
+      - intros [= ->]. lia.
+      - specialize (IHtyl i). intuition lia. }
+    rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
+    iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
+    iAssert (▷ ⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%". by rewrite -ty_size_eq.
+    iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦vl1 $H↦2]"); try done.
+    { rewrite take_length. lia. }
+    iNext; iIntros "[H↦vl1 H↦2]".
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
+    iMod ("Hr" with "H↦2") as "($ & $ & $ & $)". iApply "Hw". iNext.
+    rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
+    iSplitL "H↦pad".
+    - rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia.
+      iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
+    - iExists _. iFrame.
+  Qed.
 End case.
\ No newline at end of file