diff --git a/_CoqProject b/_CoqProject
index c00b9b3a8f964a97b26313bce06d9720693d1a22..451dd5067cf20141afdec887209e1db4745bab09 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -50,6 +50,7 @@ theories/typing/fixpoint.v
 theories/typing/type_sum.v
 theories/typing/typing.v
 theories/typing/soundness.v
+theories/typing/lib/panic.v
 theories/typing/lib/option.v
 theories/typing/lib/fake_shared_box.v
 theories/typing/lib/cell.v
@@ -78,3 +79,4 @@ 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/nonlexical.v b/theories/typing/examples/nonlexical.v
new file mode 100644
index 0000000000000000000000000000000000000000..6510eff842a4cf5f685896e2b84453363100d981
--- /dev/null
+++ b/theories/typing/examples/nonlexical.v
@@ -0,0 +1,129 @@
+From iris.proofmode Require Import tactics.
+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/function.v b/theories/typing/function.v
index 7a8d92f6003039e25e14636855b44ccc6486bfd4..44a158ad9a347d0f72abf1849ebacfd75c87a61a 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -234,8 +234,8 @@ Section typing.
 
   (* In principle, proving this hard-coded to an empty L would be sufficient --
      but then we would have to require elctx_sat as an Iris assumption. *)
-  Lemma type_call_iris' E L (κs : list lft) {A} x qκs qL tid
-        p (ps : list path) (k : expr) (fp : A → fn_params (length ps)) :
+  Lemma type_call_iris' E L (κs : list lft) {A} x (ps : list path) qκs qL tid
+        p (k : expr) (fp : A → fn_params (length ps)) :
     (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
     is_Some (to_val k) →
     lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp L qL -∗
@@ -295,8 +295,8 @@ Section typing.
         iApply (big_sepL_mono' with "Hvl"); last done. by iIntros (i [v ty']).
   Qed.
 
-  Lemma type_call_iris E (κs : list lft) {A} x qκs tid
-        f (ps : list path) (k : expr) (fp : A → fn_params (length ps)) :
+  Lemma type_call_iris E (κs : list lft) {A} x (ps : list path) qκs tid
+        f (k : expr) (fp : A → fn_params (length ps)) :
     (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) [] ((fp x).(fp_E) ϝ)) →
     is_Some (to_val k) →
     lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 45ccd39525e1086f145148a5f1a277c31306ac77..84099dd9b479054547889224f89b94540da56feb 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1076,7 +1076,7 @@ Section arc.
       iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
       iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
       rewrite -[α ⊓ ν](right_id_L).
-      iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) _ _ _ [_] with
+      iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_] with
               "LFT HE Hna Hαν Hclone [Hl H†]"); [solve_typing|solve_to_val| |].
       { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
         iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
@@ -1109,11 +1109,7 @@ Section arc.
         iExists _, _, _. iFrame "∗#". }
       iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
       iApply type_let. apply arc_drop_type. solve_typing. iIntros (drop). simpl_subst.
-      iApply (type_letcall ()); try solve_typing.
-      { (* FIXME : solve_typing should be able to do this. *)
-        move=>ϝ' /=. change (ty_outlives_E (option ty) ϝ') with (ty_outlives_E ty ϝ').
-        solve_typing. }
-      iIntros (content). simpl_subst.
+      iApply (type_letcall ()); [solve_typing..|]. iIntros (content). simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_assign; [solve_typing..|].
       iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 62224b9b19b3904adc6b89af2beda7a6d1b9220f..05e3d8315ebd17fe9b9f81b9b2a264e8091fb764 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From lrust.typing Require Import typing.
+From lrust.typing Require Import typing lib.panic.
 Set Default Proof Using "Type".
 
 Section option.
@@ -66,4 +66,30 @@ Section option.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
   Qed.
+
+  Definition option_unwrap Ï„ : val :=
+    funrec: <> ["o"] :=
+      case: !"o" of
+      [ let: "panic" := panic in
+        letcall: "r" := "panic" [] in
+        return: ["r"];
+
+        letalloc: "r" <-{Ï„.(ty_size)} !("o" +â‚— #1) in
+        delete [ #(S Ï„.(ty_size)); "o"];;
+        return: ["r"]].
+
+  Lemma option_unwrap_type Ï„ `{!TyWf Ï„} :
+    typed_val (option_unwrap τ) (fn(∅; option τ) → τ).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p=>o. simpl_subst.
+    iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+    + right. iApply type_let; [iApply panic_type|solve_typing|].
+        iIntros (panic). simpl_subst.
+      iApply (type_letcall ()); [solve_typing..|]. iIntros (r). simpl_subst.
+      iApply type_jump; solve_typing.
+    + left. iApply type_letalloc_n; [solve_typing..|]. iIntros (r). simpl_subst.
+      iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
+      iApply type_jump; solve_typing.
+  Qed.
 End option.
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
new file mode 100644
index 0000000000000000000000000000000000000000..eca8ba7cd9e147caeeb0dc568f2d999a23425724
--- /dev/null
+++ b/theories/typing/lib/panic.v
@@ -0,0 +1,25 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+(* Minimal support for panic. Lambdarust does not support unwinding
+   the stack. Instead, we just end the current thread by not calling
+   any continuation.
+
+   Note that this is not very faithfull, because e.g., [spawn] will
+   not be notified that the thread has finished. This is why we do not
+   get into trouble with [take_mut]. *)
+
+Section panic.
+  Context `{typeG Σ}.
+
+  Definition panic : val :=
+    funrec: <> [] := #().
+
+  Lemma panic_type ty `{!TyWf ty} : typed_val panic (fn(∅) → ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "!# *".
+    inv_vec args.  iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst.
+    wp_value. done.
+  Qed.
+End panic.
\ No newline at end of file
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index d51935292ecf33c42203d828397242b90202b002..a42269279bde1fe05bdeda90ac772a0c810a2d07 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1074,7 +1074,7 @@ Section code.
       wp_let. wp_let. rewrite tctx_interp_singleton tctx_hasty_val.
       iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
       rewrite -[α ⊓ ν](right_id_L).
-      iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) _ _ _ [_]
+      iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_]
               with "LFT HE Hna Hαν Hclone [H† H↦lr]"); [solve_typing|solve_to_val| |].
       { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full_S.
         iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
@@ -1107,11 +1107,7 @@ Section code.
         iFrame "∗#". auto. }
       iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
       iApply type_let. apply rc_drop_type. solve_typing. iIntros (drop). simpl_subst.
-      iApply (type_letcall ()); try solve_typing.
-      { (* FIXME : solve_typing should be able to do this. *)
-        move=>ϝ' /=. change (ty_outlives_E (option ty) ϝ') with (ty_outlives_E ty ϝ').
-        solve_typing. }
-      iIntros (content). simpl_subst.
+      iApply (type_letcall ()); [solve_typing..|]. iIntros (content). simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_assign; [solve_typing..|].
       iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 0b84223455dce1c9b862e7854833583689091802..7bceb0176a798d81140aa6ab69f8e1bbaca9a91d 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -238,7 +238,7 @@ Section ref_functions.
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
     rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
-    iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) _ _ _ [_; _]
+    iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
        with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|solve_to_val|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
       iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 020157d6e73a459dc6affee8d6c08bf69e353bee..fa27dacf60cfe8611f6ae32fca46f453371f5ea1 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -185,7 +185,7 @@ Section refmut_functions.
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
     rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
-    iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) _ _ _ [_; _]
+    iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
             with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H† Hbor]");
       [solve_typing|solve_to_val|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 9fe858a5b4a4c9eb8a4cfef4231fa2c24d051f87..e90810199698f72df905b3ed854d180f03010e87 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -99,12 +99,9 @@ Section spawn.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
         iIntros "?". by iFrame. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let. unlock.
-      iApply (type_call_iris _ [] tt 1%Qp with "LFT HE Htl [] [Hf'] [Henv]"). 4: iExact "Hf'". (* FIXME: Removing the [ ] around Hf' in the spec pattern diverges. *)
-      - solve_typing.
-      - solve_to_val.
-      - iApply lft_tok_static.
-      - iSplitL; last done. (* FIXME: iSplit should work, the RHS is persistent. *)
-        rewrite tctx_hasty_val. iApply @send_change_tid. done.
+      iApply (type_call_iris _ [] () [_] with "LFT HE Htl [] Hf' [Henv]");
+        [solve_typing|solve_to_val|iApply (lft_tok_static 1%Qp)| |].
+      - by rewrite big_sepL_singleton tctx_hasty_val send_change_tid.
       - iIntros (r) "Htl _ Hret".
         wp_rec. iApply (finish_spec with "[$Hfin Hret]"); last auto.
         by iApply @send_change_tid. }
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 4c01b97a349c1f88b488f7c889b30fa54138d9c7..9edf93f09c3ebc85269789696af454f951373221 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -20,7 +20,8 @@ Section code.
       let: "r" := new [ #0] in return: ["r"].
 
   Lemma take_type ty fty call_once `{!TyWf ty, !TyWf fty} :
-    typed_val call_once (fn(∅; fty, ty) → ty) → (* fty : FnOnce(ty) -> ty, as witnessed by the impl call_once *)
+    (* fty : FnOnce(ty) -> ty, as witnessed by the impl call_once *)
+    typed_val call_once (fn(∅; fty, ty) → ty) →
     typed_val (take ty call_once) (fn(∀ α, ∅; &uniq{α} ty, fty) → unit).
   Proof.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
@@ -30,7 +31,7 @@ Section code.
     iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (t); simpl_subst.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk (Ht & Hf' & Hx & Hx' & Henv & _)".
-    rewrite !tctx_hasty_val [[x]]lock [[env]]lock [fn _]lock. 
+    rewrite !tctx_hasty_val [[x]]lock [[env]]lock [fn _]lock.
     iDestruct (ownptr_uninit_own with "Ht") as (tl tvl) "(% & >Htl & Htl†)". subst t. simpl.
     destruct x' as [[|lx'|]|]; try done. simpl.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)"; [solve_typing..|].
@@ -41,12 +42,10 @@ Section code.
     iIntros "[Htl Hx'↦]". wp_seq.
     (* Call the function. *)
     wp_let. unlock.
-    iApply (type_call_iris _ [ϝ] tt with "LFT HE Hna [Hϝ] [Hf'] [Henv Htl Htl† Hx'vl]"). 4: iExact "Hf'". (* FIXME: Removing the [ ] around Hf' in the spec pattern diverges. *)
-    { solve_typing. }
-    { solve_to_val. }
-    { simpl. rewrite (right_id static). done. }
-    { simpl. rewrite !tctx_hasty_val. iFrame. iSplit; last done.
-      rewrite tctx_hasty_val' //. iFrame. iExists _. iFrame. }
+    iApply (type_call_iris _ [ϝ] () [_; _]
+      with "LFT HE Hna [Hϝ] Hf' [Henv Htl Htl† Hx'vl]"); [solve_typing|solve_to_val| | |].
+    { by rewrite /= (right_id static). }
+    { rewrite /= !tctx_hasty_val tctx_hasty_val' //. iFrame. iExists _. iFrame. }
     (* Prove the continuation of the function call. *)
     iIntros (r) "Hna Hϝ Hr". simpl.
     iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
@@ -66,7 +65,7 @@ Section code.
       unlock. iFrame. iExists _. rewrite uninit_own. iFrame. auto using vec_to_list_length. }
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
-    iApply (type_new _); [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_jump; solve_typing.
   Qed.
 End code.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 84d714a8360e915bea8c5492f4ad32c22c290826..26804863c4bfd3ec8231f0cbf0db2a9cea6048c0 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import list.
+From lrust.typing Require Import lft_contexts.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
@@ -242,8 +243,17 @@ Section typing.
   Lemma prod_app E L tyl1 tyl2 :
     eqtype E L (Π[Π tyl1; Π tyl2]) (Π(tyl1 ++ tyl2)).
   Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed.
+
+  Lemma ty_outlives_E_elctx_sat_product E L tyl {Wf : TyWfLst tyl} α:
+    elctx_sat E L (tyl_outlives_E tyl α) →
+    elctx_sat E L (ty_outlives_E (Π tyl) α).
+  Proof.
+    intro Hsat. eapply eq_ind; first done. clear Hsat. rewrite /ty_outlives_E /=.
+    induction Wf as [|ty [] ?? IH]=>//=. rewrite IH fmap_app //.
+  Qed.
 End typing.
 
 Arguments product : simpl never.
 Hint Opaque product : lrust_typing lrust_typing_merge.
-Hint Resolve product_mono' product_proper' : lrust_typing.
+Hint Resolve product_mono' product_proper' ty_outlives_E_elctx_sat_product
+  : lrust_typing.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 5740b779256ab42623f7bd6d29ed0119339422b5..b642ba7499cf1824e5d7a42c0eee3345a5151c95 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -262,4 +262,14 @@ Section case.
     iIntros (?? -> ??? Hr ?) "?". subst. rewrite -(Z2Nat.id i) //.
     by iApply type_seq; [eapply type_sum_memcpy_instr, Hr|done|done].
   Qed.
+
+  Lemma ty_outlives_E_elctx_sat_sum E L tyl {Wf : TyWfLst tyl} α:
+    elctx_sat E L (tyl_outlives_E tyl α) →
+    elctx_sat E L (ty_outlives_E (sum tyl) α).
+  Proof.
+    intro Hsat. eapply eq_ind; first done. clear Hsat. rewrite /ty_outlives_E /=.
+    induction Wf as [|ty [] ?? IH]=>//=. rewrite IH fmap_app //.
+  Qed.
 End case.
+
+Hint Resolve ty_outlives_E_elctx_sat_sum : lrust_typing.