diff --git a/_CoqProject b/_CoqProject
index 9d4134e7cbc428bd8b0b0a20cc61cf615ef8e347..a8156fdf6a0096eb5bdaad53dd2800d5e9c5e314 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -57,3 +57,9 @@ theories/typing/lib/refcell/ref_code.v
 theories/typing/lib/refcell/refmut_code.v
 theories/typing/lib/refcell/refmut.v
 theories/typing/lib/refcell/ref.v
+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/lazy_lft.v
+theories/typing/examples/nonlexical.v
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
new file mode 100644
index 0000000000000000000000000000000000000000..53c49df048a16b0a8d30d6f79de364ca12113742
--- /dev/null
+++ b/theories/typing/examples/get_x.v
@@ -0,0 +1,23 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section get_x.
+  Context `{typeG Σ}.
+
+  Definition get_x : val :=
+    funrec: <> ["p"] :=
+       let: "p'" := !"p" in
+       letalloc: "r" <- "p'" +ₗ #0 in
+       delete [ #1; "p"] ;; return: ["r"].
+
+  Lemma get_x_type :
+    typed_val get_x (fn(∀ α, ∅; &uniq{α}(Π[int; int])) → &shr{α}int).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
+    inv_vec p=>p. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
+    iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End get_x.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
new file mode 100644
index 0000000000000000000000000000000000000000..ceb1feb0b1fdfded6a4e6a5c1af2f153a632ddc7
--- /dev/null
+++ b/theories/typing/examples/init_prod.v
@@ -0,0 +1,28 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section init_prod.
+  Context `{typeG Σ}.
+
+  Definition init_prod : val :=
+    funrec: <> ["x"; "y"] :=
+       let: "x'" := !"x" in let: "y'" := !"y" in
+       let: "r" := new [ #2] in
+       "r" +ₗ #0 <- "x'";; "r" +ₗ #1 <- "y'";;
+       delete [ #1; "x"] ;; delete [ #1; "y"] ;; return: ["r"].
+
+  Lemma init_prod_type : typed_val init_prod (fn(∅; int, int) → Π[int;int]).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p=>x y. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
+    iApply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
+      iIntros (r). simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
+    iApply (type_assign (own_ptr 2 (uninit 1))); [solve_typing..|].
+    iApply type_assign; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End init_prod.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
new file mode 100644
index 0000000000000000000000000000000000000000..54cd056ff8a5773b26e53dd7f09aec11c5460f6b
--- /dev/null
+++ b/theories/typing/examples/lazy_lft.v
@@ -0,0 +1,44 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section lazy_lft.
+  Context `{typeG Σ}.
+
+  Definition lazy_lft : val :=
+    funrec: <> [] :=
+      Newlft;;
+      let: "t" := new [ #2] in let: "f" := new [ #1] in let: "g" := new [ #1] in
+      let: "42" := #42 in "f" <- "42";;
+      "t" +ₗ #0 <- "f";; "t" +ₗ #1 <- "f";;
+      let: "t0'" := !("t" +ₗ #0) in "t0'";;
+      let: "23" := #23 in "g" <- "23";;
+      "t" +ₗ #1 <- "g";;
+      let: "r" := new [ #0] in
+      Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; return: ["r"].
+
+  Lemma lazy_lft_type : typed_val lazy_lft (fn(∅) → unit).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p. simpl_subst.
+    iApply (type_newlft []). iIntros (α).
+    iApply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
+      iIntros (t). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (f). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (g). simpl_subst.
+    iApply type_int. iIntros (v42). simpl_subst.
+    iApply type_assign; [solve_typing..|].
+    iApply (type_assign _ (&shr{α}_)); [solve_typing..|].
+    iApply type_assign; [solve_typing..|].
+    iApply type_deref; [solve_typing..|]. iIntros (t0'). simpl_subst.
+    iApply type_letpath; [solve_typing|]. iIntros (dummy). simpl_subst.
+    iApply type_int. iIntros (v23). simpl_subst.
+    iApply type_assign; [solve_typing..|].
+    iApply (type_assign _ (&shr{α}int)); [solve_typing..|].
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_endlft; [solve_typing..|].
+    iApply (type_delete (Π[&shr{α}_;&shr{α}_])%T); [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End lazy_lft.
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
new file mode 100644
index 0000000000000000000000000000000000000000..91141690987ae86ac47a0066482a86dba24098e2
--- /dev/null
+++ b/theories/typing/examples/nonlexical.v
@@ -0,0 +1,128 @@
+From lrust.typing Require Import typing lib.option.
+
+(* Typing "problem case #3" from:
+     http://smallcultfollowing.com/babysteps/blog/2016/04/27/non-lexical-lifetimes-introduction/
+
+  Differences with the original implementation:
+
+   We ignore dropping.
+   We have to add a Copy bound on the key type.
+   We do not support panic, hence we do not support option::unwrap. We use
+   unwrap_or as a replacement.
+*)
+
+Section non_lexical.
+  Context `{typeG Σ} (HashMap K V : type)
+          `{!TyWf hashmap, !TyWf K, !TyWf V, !Copy K}
+          (defaultv get_mut insert: val).
+
+  Hypothesis defaultv_type :
+    typed_val defaultv (fn(∅) → V).
+
+  Hypothesis get_mut_type :
+    typed_val get_mut (fn(∀ '(α, β), ∅; &uniq{α} hashmap, &shr{β} K) →
+                       option (&uniq{α} V)).
+
+  Hypothesis insert_type :
+    typed_val insert (fn(∀ α, ∅; &uniq{α} hashmap, K, V) → option V).
+
+  Definition get_default : val :=
+    funrec: <> ["map"; "key"] :=
+      let: "get_mut" := get_mut in
+      let: "map'" := !"map" in
+
+      Newlft;;
+
+      Newlft;;
+      letalloc: "map0" <- "map'" in
+      letalloc: "key0" <- "key" in
+      letcall: "o" := "get_mut" ["map0"; "key0"]%E in
+      Endlft;;
+    withcont: "k":
+      case: !"o" of
+      [ (* None *)
+        Endlft;;
+
+        let: "insert" := insert in
+        Newlft;;
+        letalloc: "map0" <- "map'" in
+        letalloc: "key0" <-{K.(ty_size)} !"key" in
+        let: "defaultv" := defaultv in
+        letcall: "default0" := "defaultv" [] in
+        letcall: "old" := "insert" ["map0"; "key0"; "default0"]%E in
+        Endlft;;
+        delete [ #(option V).(ty_size); "old"];; (* We should drop here. *)
+
+        Newlft;;
+        letalloc: "map0" <- "map'" in
+        letalloc: "key0" <- "key" in
+        letcall: "r'" := "get_mut" ["map0"; "key0"]%E in
+        Endlft;;
+        let: "unwrap" := option_unwrap (&uniq{static}V) in
+        letcall: "r" := "unwrap" ["r'"]%E in
+        "k" ["r"];
+
+        (* Some *)
+        letalloc: "r" <-{1} !("o" +ₗ #1) in
+        "k" ["r"]
+      ]
+    cont: "k" ["r"] :=
+      delete [ #(option (&uniq{static}V)).(ty_size); "o"];;
+      delete [ #1; "map"];; delete [ #K.(ty_size); "key"];; (* We should drop key here *)
+      return: ["r"].
+
+    Lemma get_default_type :
+      typed_val get_default (fn(∀ m, ∅; &uniq{m} hashmap, K) → &uniq{m} V).
+    Proof.
+      intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+        iIntros (m ϝ ret p). inv_vec p=>map key. simpl_subst.
+      iApply type_let; [iApply get_mut_type|solve_typing|].
+        iIntros (get_mut'). simpl_subst.
+      iApply type_deref; [solve_typing..|]. iIntros (map'). simpl_subst.
+      iApply (type_newlft [m]). iIntros (κ).
+      iApply (type_newlft [ϝ]). iIntros (α).
+      iApply (type_letalloc_1 (&uniq{κ}_)); [solve_typing..|]. iIntros (map0). simpl_subst.
+      iApply (type_letalloc_1 (&shr{α}K)); [solve_typing..|]. iIntros (key0). simpl_subst.
+      iApply (type_letcall (κ, α)); [solve_typing..|]. iIntros (o). simpl_subst.
+      iApply type_endlft.
+      iApply (type_cont [_] [ϝ ⊑ₗ []]
+            (λ r, [o ◁ box (Π[uninit 1;uninit 1]); map ◁ box (uninit 1);
+                   key ◁ box K; r!!!0 ◁ box (&uniq{m} V)])).
+      { iIntros (k). simpl_subst.
+        iApply type_case_own;
+          [solve_typing| constructor; [|constructor; [|constructor]]; left].
+        - iApply type_endlft.
+          iApply type_let; [iApply insert_type|solve_typing|].
+            iIntros (insert'). simpl_subst.
+          iApply (type_newlft [ϝ]). iIntros (β). clear map0 key0.
+          iApply (type_letalloc_1 (&uniq{β}_)); [solve_typing..|].
+            iIntros (map0). simpl_subst.
+          iApply (type_letalloc_n _(box K)); [solve_typing..|]. iIntros (key0). simpl_subst.
+          iApply type_let; [iApply defaultv_type|solve_typing|].
+            iIntros (defaultv'). simpl_subst.
+          iApply (type_letcall ()); [solve_typing..|]. iIntros (default0). simpl_subst.
+          iApply (type_letcall β); [solve_typing..|]. iIntros (old). simpl_subst.
+          iApply type_endlft.
+          iApply type_delete; [solve_typing..|].
+          iApply (type_newlft [ϝ]). iIntros (γ). clear map0 key0.
+          iApply (type_letalloc_1 (&uniq{m}_)); [solve_typing..|].
+            iIntros (map0). simpl_subst.
+          iApply (type_letalloc_1 (&shr{γ}K)); [solve_typing..|].
+            iIntros (key0). simpl_subst.
+          iApply (type_letcall (m, γ)); [solve_typing..|]. iIntros (r'). simpl_subst.
+          iApply type_endlft.
+          iApply type_let; [iApply (option_unwrap_type (&uniq{m}V))|solve_typing|].
+            iIntros (unwrap'). simpl_subst.
+          iApply (type_letcall ()); [solve_typing..|]. iIntros (r). simpl_subst.
+          iApply type_jump; solve_typing.
+        - iApply type_equivalize_lft.
+          iApply (type_letalloc_n (&uniq{m}V) (own_ptr _ (&uniq{m}V))); [solve_typing..|].
+            iIntros (r). simpl_subst.
+          iApply type_jump; solve_typing. }
+      iIntros "!# *". inv_vec args=>r. simpl_subst.
+      iApply type_delete; [solve_typing..|].
+      iApply type_delete; [solve_typing..|].
+      iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+    Qed.
+End non_lexical.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
new file mode 100644
index 0000000000000000000000000000000000000000..aeb0740cac53778e41ff7dc51d9dc0ffd6458798
--- /dev/null
+++ b/theories/typing/examples/rebor.v
@@ -0,0 +1,36 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section rebor.
+  Context `{typeG Σ}.
+
+  Definition rebor : val :=
+    funrec: <> ["t1"; "t2"] :=
+       Newlft;;
+       letalloc: "x" <- "t1" in
+       let: "x'" := !"x" in let: "y" := "x'" +ₗ #0 in
+       "x" <- "t2";;
+       let: "y'" := !"y" in
+       letalloc: "r" <- "y'" in
+       Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
+                 delete [ #1; "x"] ;; return: ["r"].
+
+  Lemma rebor_type :
+    typed_val rebor (fn(∅; Π[int; int], Π[int; int]) → int).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p=>t1 t2. simpl_subst.
+    iApply (type_newlft []). iIntros (α).
+    iApply (type_letalloc_1 (&uniq{α}(Π[int; int]))); [solve_typing..|]. iIntros (x). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply (type_letpath (&uniq{α}int)); [solve_typing|]. iIntros (y). simpl_subst.
+    iApply (type_assign _ (&uniq{α}(Π[int; int]))); [solve_typing..|].
+    iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
+    iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_endlft.
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End rebor.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
new file mode 100644
index 0000000000000000000000000000000000000000..302b78833add5ef989c6844d1a5618bf749ab0e2
--- /dev/null
+++ b/theories/typing/examples/unbox.v
@@ -0,0 +1,24 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section unbox.
+  Context `{typeG Σ}.
+
+  Definition unbox : val :=
+    funrec: <> ["b"] :=
+       let: "b'" := !"b" in let: "bx" := !"b'" in
+       letalloc: "r" <- "bx" +ₗ #0 in
+       delete [ #1; "b"] ;; return: ["r"].
+
+  Lemma ubox_type :
+    typed_val unbox (fn(∀ α, ∅; &uniq{α}(box(Π[int; int]))) → &uniq{α}int).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret b). inv_vec b=>b. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (b'); simpl_subst.
+    iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
+    iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End unbox.