diff --git a/_CoqProject b/_CoqProject
index bc8a28e2a8203cabc1ba8399cc3abb6d1e6a2648..828e6d1f8f6d66ab27037f0a8400aeed750b4bfc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -45,6 +45,7 @@ theories/typing/fixpoint.v
 theories/typing/type_sum.v
 theories/typing/typing.v
 theories/typing/soundness.v
+theories/typing/option.v
 theories/typing/unsafe/cell.v
 theories/typing/unsafe/spawn.v
 theories/typing/unsafe/refcell/refcell.v
@@ -57,6 +58,5 @@ theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v
 theories/typing/examples/unbox.v
 theories/typing/examples/init_prod.v
-theories/typing/examples/option_as_mut.v
 theories/typing/examples/unwrap_or.v
 theories/typing/examples/lazy_lft.v
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index db14c7eb5359205899a706aad4c9d000fef0032b..e6c440cd240f8a43dac0be026d0d269256f3623d 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 1d1eefc04f803173d5a038eb4c3ab0a461bfa88f..c307f3a96b79465d976a3919be63f2bb45f8e4c1 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 96c2d0ee45707f2c041554b45568d0baaaf809a8..16869ee69712c32d5bfd92e7d116f4923b79b893 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 99254956e39c99c28918601b1a5c0b99134fc95f..67a7632b7425b121155b2f0aa2d43c6fc1be830b 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 0aeb0f71a2fc93e43f8db78adca4c7fcfcaa495d..4c99656ee226f1290478b9d0dd46f7e862d09328 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/unwrap_or.v b/theories/typing/examples/unwrap_or.v
deleted file mode 100644
index dcb45785422a78ce8f74a1ad224ac53d09f9c631..0000000000000000000000000000000000000000
--- a/theories/typing/examples/unwrap_or.v
+++ /dev/null
@@ -1,30 +0,0 @@
-From iris.proofmode Require Export tactics.
-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section unwrap_or.
-  Context `{typeG Σ}.
-
-  Definition unwrap_or Ï„ : val :=
-    funrec: <> ["o"; "def"] :=
-      case: !"o" of
-      [ delete [ #(S Ï„.(ty_size)); "o"];; "return" ["def"];
-        letalloc: "r" <-{Ï„.(ty_size)} !("o" +â‚— #1) in
-        delete [ #(S Ï„.(ty_size)); "o"];; delete [ #Ï„.(ty_size); "def"];; "return" ["r"]].
-
-  Lemma unwrap_or_type Ï„ :
-    typed_instruction_ty [] [] [] (unwrap_or Ï„)
-        (fn([]; Σ[unit; τ], τ) → τ).
-  Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
-      inv_vec p=>o def. simpl_subst.
-    iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
-    + right. iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing.
-    + left. iApply type_letalloc_n; [solve_typing|by apply read_own_move|]. iIntros (r).
-        simpl_subst.
-      iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
-      iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing.
-  Qed.
-End unwrap_or.
diff --git a/theories/typing/examples/option_as_mut.v b/theories/typing/option.v
similarity index 53%
rename from theories/typing/examples/option_as_mut.v
rename to theories/typing/option.v
index 652d93eaee56c7fe3ae0e687e064b44c60ff5c3e..86ac155dde5763b133de5837391ceae2d5d1f806 100644
--- a/theories/typing/examples/option_as_mut.v
+++ b/theories/typing/option.v
@@ -1,10 +1,12 @@
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
-Section option_as_mut.
+Section option.
   Context `{typeG Σ}.
 
+  Definition option (τ : type) := Σ[unit; τ]%T.
+
   Definition option_as_mut : val :=
     funrec: <> ["o"] :=
       let: "o'" := !"o" in
@@ -17,7 +19,7 @@ Section option_as_mut.
 
   Lemma option_as_mut_type Ï„ :
     typed_instruction_ty [] [] [] option_as_mut
-        (fn(∀ α, [☀α]; &uniq{α} Σ[unit; τ]) → Σ[unit; &uniq{α}τ]).
+        (fn(∀ α, [☀α]; &uniq{α} (option τ)) → option (&uniq{α}τ)).
   Proof.
     iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
       inv_vec p=>o. simpl_subst.
@@ -36,4 +38,30 @@ Section option_as_mut.
       iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
   Qed.
-End option_as_mut.
+
+  Definition option_unwrap_or Ï„ : val :=
+    funrec: <> ["o"; "def"] :=
+      case: !"o" of
+      [ delete [ #(S Ï„.(ty_size)); "o"];;
+        "return" ["def"];
+
+        letalloc: "r" <-{Ï„.(ty_size)} !("o" +â‚— #1) in
+        delete [ #(S Ï„.(ty_size)); "o"];; delete [ #Ï„.(ty_size); "def"];;
+        "return" ["r"]].
+
+  Lemma option_unwrap_or_type Ï„ :
+    typed_instruction_ty [] [] [] (option_unwrap_or Ï„)
+        (fn([]; option τ, τ) → τ).
+  Proof.
+    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+      inv_vec p=>o def. simpl_subst.
+    iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+    + right. iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing.
+    + left. iApply type_letalloc_n; [solve_typing|by apply read_own_move|]. iIntros (r).
+        simpl_subst.
+      iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
+      iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing.
+  Qed.
+End option.
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 5c7e4844827ee9d001e2eb26946784502663f46c..5a12ad7f7a876cf68274f5030851e6ba20575ef4 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
-From lrust.typing Require Import typing.
+From lrust.typing Require Import typing option.
 From lrust.typing.unsafe.refcell Require Import refcell ref refmut.
 Set Default Proof Using "Type".
 
@@ -130,14 +130,14 @@ Section refcell_functions.
       let: "x'" := !"x" in
       let: "n" := !"x'" in
       if: "n" ≤ #-1 then
-        "r" <-{Σ 1} ();;
+        "r" <-{Σ 0} ();;
         "k" ["r"] (* FIXME RJ: this is very confusing, "k" does not even look like it is bound here... *)
       else
         "x'" <- "n" + #1;;
         let: "ref" := new [ #2 ] in
         "ref" <- "x'" +â‚— #1;;
         "ref" +â‚— #1 <- "x'";;
-        "r" <-{2,Σ 0} !"ref";;
+        "r" <-{2,Σ 1} !"ref";;
         delete [ #2; "ref"];;
         "k" ["r"]
       cont: "k" ["r"] :=
@@ -145,12 +145,12 @@ Section refcell_functions.
 
   Lemma refcell_try_borrow_type ty :
     typed_instruction_ty [] [] [] refcell_try_borrow
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[ref α ty; unit])%T).
+        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (ref α ty))%T).
   Proof.
     iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
       inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
-                                    r!!!0 ◁ box Σ[ref α ty; unit]])%TC);
+                                    r!!!0 ◁ box (option (ref α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing. }
@@ -171,7 +171,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [ref α ty; unit]);
+      iApply (type_sum_assign_unit [unit; ref α ty]);
         [solve_typing..|by eapply write_own|]; first last.
       simpl. iApply (type_jump [_]); solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
@@ -223,7 +223,7 @@ Section refcell_functions.
         iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
         iApply lft_glb_mono. done. iApply lft_incl_refl. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [ref α ty; unit]);
+      iApply (type_sum_memcpy [unit; ref α ty]);
         [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
@@ -240,23 +240,23 @@ Section refcell_functions.
         let: "ref" := new [ #2 ] in
         "ref" <- "x'" +â‚— #1;;
         "ref" +â‚— #1 <- "x'";;
-        "r" <-{2,Σ 0} !"ref";;
+        "r" <-{2,Σ 1} !"ref";;
         delete [ #2; "ref"];;
         "k" ["r"]
       else
-        "r" <-{Σ 1} ();;
+        "r" <-{Σ 0} ();;
         "k" ["r"]
       cont: "k" ["r"] :=
         delete [ #1; "x"];; "return" ["r"].
 
   Lemma refcell_try_borrow_mut_type ty :
     typed_instruction_ty [] [] [] refcell_try_borrow_mut
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[refmut α ty; unit])%T).
+        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (refmut α ty))%T).
   Proof.
     iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
       inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
-                                    r!!!0 ◁ box Σ[refmut α ty; unit]])%TC);
+                                    r!!!0 ◁ box (option (refmut α ty))]%TC));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
@@ -295,7 +295,7 @@ Section refcell_functions.
         iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
         iApply lft_glb_mono; first done. iApply lft_incl_refl. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [refmut α ty; unit]);
+      iApply (type_sum_memcpy [unit; refmut α ty]);
         [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
@@ -306,7 +306,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [refmut α ty; unit]);
+      iApply (type_sum_assign_unit [unit; refmut α ty]);
         [solve_typing..|by eapply write_own|].
       simpl. iApply (type_jump [_]); solve_typing.
   Qed.