diff --git a/_CoqProject b/_CoqProject
index e0d8ab8b51d57fd4b1b0be8831c10ec46a98d119..40ecd9a46c6484165bc734b27892b8c2d797a354 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -41,3 +41,4 @@ theories/typing/programs.v
 theories/typing/borrow.v
 theories/typing/cont.v
 theories/typing/fixpoint.v
+theories/typing/case.v
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 05c665b19ee35cf23a400b4068a245226e6b8384..62342edc46359eaf6c09266eb066f7dd7bdc24e9 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -295,7 +295,7 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
               []
 | CaseS i el e σ :
     0 ≤ i →
-    nth_error el (Z.to_nat i) = Some e →
+    el !! (Z.to_nat i) = Some e →
     head_step (Case (Lit $ LitInt i) el) σ e σ []
 | ForkS e σ:
     head_step (Fork e) σ (Lit LitUnit) σ [e].
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index f0c96434453723966dd908574f62adf9c8641f33..cfd392c0dd3578783a1f185236bdbaecbc0cd047 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -178,7 +178,7 @@ Qed.
 
 Lemma wp_case E i e el Φ :
   0 ≤ i →
-  nth_error el (Z.to_nat i) = Some e →
+  el !! (Z.to_nat i) = Some e →
   ▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
 Proof.
   iIntros (??) "?". iApply ownP_lift_pure_det_head_step; eauto.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 3b6930650355e84fcbad1e358313045623fc0118..af9528f2a9ab97b29d3d5d4fc5cacb72c2655080 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -23,10 +23,8 @@ Notation "'case:' e0 'of' el" := (Case e0%E el%E)
 Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
   (at level 200, e1, e2, e3 at level 200) : expr_scope.
 Notation "()" := LitUnit : val_scope.
-Notation "! e" := (Read Na1Ord e%E)
-  (at level 9, right associativity) : expr_scope.
-Notation "!ˢᶜ e" := (Read ScOrd e%E)
-  (at level 9, right associativity) : expr_scope.
+Notation "! e" := (Read Na1Ord e%E) (at level 9, format "! e") : expr_scope.
+Notation "!ˢᶜ e" := (Read ScOrd e%E) (at level 9, format "!ˢᶜ e") : expr_scope.
 Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
   (at level 50, left associativity) : expr_scope.
 Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
diff --git a/theories/typing/case.v b/theories/typing/case.v
new file mode 100644
index 0000000000000000000000000000000000000000..138b408050f1e2e2786082b4524541c1a0779b05
--- /dev/null
+++ b/theories/typing/case.v
@@ -0,0 +1,125 @@
+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import heap.
+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.
+
+Section case.
+  Context `{typeG Σ}.
+
+  (* FIXME : the doc does not give [p +ₗ #(S (ty.(ty_size))) ◁ ...]. *)
+  Lemma type_case_own E L C T p n tyl el:
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
+         (p +ₗ #(S (ty.(ty_size))) ◁
+            own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T) e ∨
+      typed_body E L C ((p ◁ own n (sum tyl)) :: T) e) tyl el →
+    typed_body E L C ((p ◁ own n (sum tyl)) :: T) (case: !p of el).
+  Proof.
+    iIntros (Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+    rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
+    iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
+    iDestruct "Hp" as (l) "[EQ [H↦ Hf]]". iDestruct "EQ" as %[=->].
+    iDestruct "H↦" as (vl) "[H↦ Hown]".
+    iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
+    simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
+    rewrite -Nat.add_1_l app_length -!freeable_sz_split
+            heap_mapsto_vec_cons heap_mapsto_vec_app.
+    iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
+    iDestruct "Hf" as "(Hfi & Hfvl' & Hfvl'')".
+    rewrite nth_lookup.
+    destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
+    edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
+    wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
+    destruct Hety as [Hety|Hety]; iApply (Hety with "HEAP LFT Hna HE HL HC");
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
+    - iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
+      iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
+      + rewrite shift_loc_0. iExists _. iFrame. iSplit. done. iExists [ #i].
+        rewrite heap_mapsto_vec_singleton.
+        iFrame. iExists [_], []. auto.
+      + iExists _. iFrame. iSplit. done. iExists _. iFrame.
+      + rewrite -EQlen app_length minus_plus uninit_sz -(shift_loc_assoc_nat _ 1).
+        iExists _. iFrame. iSplit. done. iExists _. iFrame. rewrite uninit_own. auto.
+    - iExists _. iSplit. done.
+      assert (EQf:=freeable_sz_split n 1). simpl in EQf. rewrite -EQf. clear EQf.
+      rewrite -EQlen app_length -freeable_sz_split. iFrame.
+      iExists (#i :: vl' ++ vl''). iNext.
+      rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
+      iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty. auto.
+  Qed.
+
+  Lemma type_case_uniq E L C T p κ tyl el:
+    lctx_lft_alive E L κ →
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e ∨
+      typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) e) tyl el →
+    typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) (case: !p of el).
+  Proof.
+    iIntros (Halive Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+    rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
+    iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
+    iDestruct "Hp" as (l P) "[[EQ HP] Hb]". iDestruct "EQ" as %[=->].
+    iMod (bor_iff with "LFT HP Hb") as "Hb". done.
+    iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
+    iMod (bor_acc_cons with "LFT Hb Htok") as "[H↦ Hclose']". done.
+    iDestruct "H↦" as (vl) "[H↦ Hown]".
+    iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
+    iDestruct "EQlen" as %[=EQlen].
+    rewrite heap_mapsto_vec_cons heap_mapsto_vec_app nth_lookup.
+    iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
+    destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
+    edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
+    wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
+    iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'.
+    destruct Hety as [Hety|Hety].
+    - iMod ("Hclose'" $! (shift_loc l 1 ↦∗: ty.(ty_own) tid)%I
+            with "[H↦vl' Hown] [H↦i H↦vl'']") as "[Hb Htok]".
+      { iExists vl'. iFrame. }
+      { iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
+        iExists (#i::vl'2++vl''). iIntros "!>". iNext.
+        iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
+        rewrite heap_mapsto_vec_cons heap_mapsto_vec_app EQlenvl' EQlenvl'2.
+        iFrame. iExists _, _, _. iSplit. by auto.
+        rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
+      iMod ("Hclose" with "Htok") as "[HE HL]".
+      iApply (Hety with "HEAP LFT Hna HE HL HC").
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame "HT".
+      iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
+    - iMod ("Hclose'" with "* [H↦i H↦vl' H↦vl'' Hown] []") as "[Hb Htok]";
+        [|by iIntros "!>$"|].
+      { iExists (#i::vl'++vl'').
+        rewrite heap_mapsto_vec_cons heap_mapsto_vec_app -EQlen. iFrame. iNext.
+        iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
+      iMod ("Hclose" with "Htok") as "[HE HL]".
+      iApply (Hety with "HEAP LFT Hna HE HL HC").
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame "HT".
+      iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
+  Qed.
+
+  Lemma type_case_shr E L C T p κ tyl el:
+    lctx_lft_alive E L κ →
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e ∨
+      typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) e) tyl el →
+    typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) (case: !p of el).
+  Proof.
+    iIntros (Halive Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+    rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
+    iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
+    iDestruct "Hp" as (l) "[EQ Hl]". iDestruct "EQ" as %[=->].
+    iDestruct "Hl" as (i) "[#Hb Hshr]".
+    iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
+    iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
+    rewrite nth_lookup.
+    destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hshr" as "[]".
+    edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
+    wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
+    iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
+    iMod ("Hclose" with "Htok") as "[HE HL]".
+    destruct Hety as [Hety|Hety]; iApply (Hety with "HEAP LFT Hna HE HL HC");
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
+    - iExists _. auto.
+    - iExists _. iSplit. done. iExists i. rewrite nth_lookup EQty /=. auto.
+  Qed.
+End case.
\ No newline at end of file
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 367c3ab7e8e5a7c0ab8d99bd70d2b00a324d0356..60b534d250e5e8c380a583531b315b6c2f9d9e58 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -16,6 +16,7 @@ Section own.
     | sz, n => †{mk_Qp (sz / n) _}l…sz
     end%I.
   Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
+  Arguments freeable_sz : simpl never.
   Global Instance freable_sz_timeless n sz l : TimelessP (freeable_sz n sz l).
   Proof. destruct sz, n; apply _. Qed.
 
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 2f33dc402f5010b668a9078bf048d7ce1d43ecd1..4adb9c5134151815aea8edd47ec912a6462272bb 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -42,13 +42,12 @@ Section sum.
   Definition list_max (l : list nat) := foldr max 0%nat l.
 
   Definition is_pad i tyl (vl : list val) : iProp Σ :=
-    ⌜((nth i tyl ∅).(ty_size) + length vl)%nat =
-                                         (list_max $ map ty_size $ tyl)⌝%I.
+    ⌜((nth i tyl ∅).(ty_size) + length vl)%nat = (list_max $ map ty_size tyl)⌝%I.
 
   Lemma split_sum_mt l tid q tyl :
     (l ↦∗{q}: λ vl,
          ∃ (i : nat) vl' vl'', ⌜vl = #i :: vl' ++ vl''⌝ ∗
-                               ⌜length vl = S (list_max $ map ty_size $ tyl)⌝ ∗
+                               ⌜length vl = S (list_max $ map ty_size tyl)⌝ ∗
                                ty_own (nth i tyl ∅) tid vl')%I
     ⊣⊢ ∃ (i : nat), (l ↦{q} #i ∗
                        shift_loc l (S $ (nth i tyl ∅).(ty_size)) ↦∗{q}: is_pad i tyl) ∗
@@ -75,10 +74,10 @@ Section sum.
   Qed.
 
   Program Definition sum (tyl : list type) :=
-    {| ty_size := S (list_max $ map ty_size $ tyl);
+    {| ty_size := S (list_max $ map ty_size tyl);
        ty_own tid vl :=
          (∃ (i : nat) vl' vl'', ⌜vl = #i :: vl' ++ vl''⌝ ∗
-                                ⌜length vl = S (list_max $ map ty_size $ tyl)⌝ ∗
+                                ⌜length vl = S (list_max $ map ty_size tyl)⌝ ∗
                                 (nth i tyl ∅).(ty_own) tid vl')%I;
        ty_shr κ tid l :=
          (∃ (i : nat),
@@ -122,9 +121,9 @@ Section sum.
         edestruct @Forall2_lookup_l as (ty2 & Hl2 & Hty2); [done..|].
         rewrite (nth_lookup_Some tyl2 _ _ ty2) //.
         by iApply (Hty2 with "* [] []"). }
-    clear -Hleq. iSplit; last (iSplit; iAlways).
-    - simpl. by rewrite Hleq. 
-    - iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+    clear -Hleq. iSplit; last iSplit.
+    - simpl. by rewrite Hleq.
+    - iNext. iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
       iExists i, vl', vl''. iSplit; first done.
       iSplit; first by rewrite -Hleq.
       iDestruct ("Hty" $! i) as "(_ & #Htyi & _)". by iApply "Htyi".