diff --git a/_CoqProject b/_CoqProject
index 42ca85c..45f39cf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -69,10 +69,12 @@ theories/type_systems/systemf_mu_state/locations.v
 theories/type_systems/systemf_mu_state/lang.v
 theories/type_systems/systemf_mu_state/notation.v
 theories/type_systems/systemf_mu_state/types.v
+theories/type_systems/systemf_mu_state/types_sol.v
 theories/type_systems/systemf_mu_state/tactics.v
 theories/type_systems/systemf_mu_state/execution.v
 theories/type_systems/systemf_mu_state/parallel_subst.v
 theories/type_systems/systemf_mu_state/logrel.v
+theories/type_systems/systemf_mu_state/logrel_sol.v
 
 # By removing the # below, you can add the exercise sheets to make
 #theories/type_systems/warmup/warmup.v
@@ -92,3 +94,4 @@ theories/type_systems/systemf_mu_state/logrel.v
 #theories/type_systems/systemf_mu/exercises06.v
 #theories/type_systems/systemf_mu/exercises06_sol.v
 #theories/type_systems/systemf_mu_state/exercises07.v
+#theories/type_systems/systemf_mu_state/exercises07_sol.v
diff --git a/theories/type_systems/systemf_mu_state/exercises07_sol.v b/theories/type_systems/systemf_mu_state/exercises07_sol.v
new file mode 100644
index 0000000..80c9047
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/exercises07_sol.v
@@ -0,0 +1,202 @@
+From iris Require Import prelude.
+From semantics.ts.systemf_mu_state Require Import lang notation parallel_subst tactics execution.
+
+(** * Exercise Sheet 7 *)
+
+(** Exercise 1: Stack (LN Exercise 45) *)
+(* We use lists to model our stack *)
+Section lists.
+  Context (A : type).
+  Definition list_type : type :=
+    μ: Unit + (A.[ren (+1)] × #0).
+
+  Definition nil_val : val :=
+    RollV (InjLV (LitV LitUnit)).
+  Definition cons_val (v : val) (xs : val) : val :=
+    RollV (InjRV (v, xs)).
+  Definition cons_expr (v : expr) (xs : expr) : expr :=
+    roll (InjR (v, xs)).
+
+  Definition list_case : val :=
+    Λ, λ: "l" "n" "hf", match: unroll "l" with InjL <> => "n" | InjR "h" => "hf" (Fst "h") (Snd "h") end.
+
+  Lemma nil_val_typed Σ n Γ :
+    type_wf n A →
+    TY Σ; n; Γ ⊢ nil_val : list_type.
+  Proof.
+    intros. solve_typing.
+  Qed.
+
+  Lemma cons_val_typed Σ n Γ (v xs : val) :
+    type_wf n A →
+    TY Σ; n; Γ ⊢ v : A →
+    TY Σ; n; Γ ⊢ xs : list_type →
+    TY Σ; n; Γ ⊢ cons_val v xs : list_type.
+  Proof.
+    intros. simpl. solve_typing.
+  Qed.
+
+  Lemma cons_expr_typed Σ n Γ (x xs : expr) :
+    type_wf n A →
+    TY Σ; n; Γ ⊢ x : A →
+    TY Σ; n; Γ ⊢ xs : list_type →
+    TY Σ; n; Γ ⊢ cons_expr x xs : list_type.
+  Proof.
+    intros. simpl. solve_typing.
+  Qed.
+
+  Lemma list_case_typed Σ n Γ :
+    type_wf n A →
+    TY Σ; n; Γ ⊢ list_case : (∀: list_type.[ren (+1)] → #0 → (A.[ren(+1)] → list_type.[ren (+1)] → #0) → #0).
+  Proof.
+    intros. simpl. solve_typing.
+  Qed.
+End lists.
+
+(* The stack interface *)
+Definition stack_t A : type :=
+  ∃: ((Unit → #0)       (* new *)
+    × (#0 → A.[ren (+1)] → Unit)   (* push *)
+    × (#0 → Unit + A.[ren (+1)]))  (* pop *)
+  .
+
+(** We assume an abstract implementation of lists (an example implementation is provided above) *)
+Definition list_t (A : type) : type :=
+  ∃: (#0 (* mynil *)
+    × (A.[ren (+1)] → #0 → #0) (* mycons *)
+    × (∀: #1 → #0 → (A.[ren (+2)] → #1 → #0) → #0)) (* mylistcase *)
+  .
+
+Definition mystack : val :=
+  (* define your stack implementation, assuming "lc" is a list implementation *)
+  λ: "lc", 
+  ((λ: <>, New (Fst (Fst "lc"))),
+   (λ: "st" "el",
+      let: "stv" := !"st" in
+      "st" <- Snd (Fst "lc") "el" "stv"),
+   (λ: "st",
+      let: "stv" := !"st" in
+      (Snd "lc") <> "stv" (InjL #())%V (λ: "h" "rstv",
+        "st" <- "rstv";;
+        InjR "h"))).
+
+Definition make_mystack : val :=
+  Λ, λ: "lc",
+    unpack "lc" as "lc" in
+    pack (mystack "lc").
+
+Lemma make_mystack_typed Σ n Γ :
+  TY Σ; n; Γ ⊢ make_mystack : (∀: list_t #0 → stack_t #0).
+Proof.
+  repeat solve_typing_fast.
+Qed.
+
+
+(** Exercise 2 (LN Exercise 46): Obfuscated code *)
+Definition obf_expr : expr :=
+  let: "x" := new (λ: "x", "x" + "x") in
+  let: "f" := (λ: "g", let: "f" := !"x" in "x" <- "g";; "f" #11) in
+  "f" (λ: "x", "f" (λ: <>, "x")) + "f" (λ: "x", "x" + #9).
+
+(* The following contextual lifting lemma will be helpful *)
+Lemma rtc_contextual_step_fill K e e' h h' :
+  rtc contextual_step (e, h) (e', h') →
+  rtc contextual_step (fill K e, h) (fill K e', h').
+Proof.
+  remember (e, h) as a eqn:Heqa. remember (e', h') as b eqn:Heqb.
+  induction 1 as [ | ? c ? Hstep ? IH] in e', h', e, h, Heqa, Heqb |-*; subst.
+  - simplify_eq. done.
+  - destruct c as (e1, h1).
+    econstructor 2.
+    + apply fill_contextual_step. apply Hstep.
+    + apply IH; done.
+Qed.
+
+(* You may use the [new_fresh] and [init_heap_singleton] lemmas to allocate locations *)
+
+Lemma obf_expr_eval :
+  ∃ h', rtc contextual_step (obf_expr, ∅) (of_val #42, h').
+Proof.
+  eexists. unfold obf_expr.
+  econstructor 2.
+  { eapply fill_contextual_step with (K := [AppRCtx _]).
+    eapply base_contextual_step.
+    eapply (new_fresh (LamV _ _)).
+  }
+  rewrite init_heap_singleton.
+  simpl.
+  econstructor 2.
+  { apply base_contextual_step. econstructor; done. }
+  simpl.
+  econstructor 2.
+  { apply base_contextual_step. econstructor; done. }
+  simpl. etrans.
+  { apply rtc_contextual_step_fill with (K := [BinOpRCtx _ _]).
+    econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    simpl. econstructor 2.
+    { apply fill_contextual_step with (K := [AppRCtx _]).
+      apply base_contextual_step.
+      econstructor. rewrite lookup_insert. done.
+    }
+    simpl. econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    simpl. econstructor 2.
+    { apply fill_contextual_step with (K := [AppRCtx _]).
+      apply base_contextual_step. econstructor; done.
+    }
+    rewrite insert_insert. simpl. econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    simpl. econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    simpl. econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    reflexivity.
+  }
+  simpl. etrans.
+  { apply rtc_contextual_step_fill with (K := [BinOpLCtx _ (LitV _)]).
+    econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    simpl. econstructor 2.
+    { apply fill_contextual_step with (K := [AppRCtx _]).
+      apply base_contextual_step.
+      econstructor. rewrite lookup_insert. done.
+    }
+    simpl. econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    simpl. econstructor 2.
+    { apply fill_contextual_step with (K := [AppRCtx _]).
+      apply base_contextual_step. econstructor; done.
+    }
+    rewrite insert_insert. simpl. econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    simpl. econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    simpl. econstructor 2.
+    { apply base_contextual_step. econstructor; done. }
+    reflexivity.
+  }
+  simpl.
+  econstructor 2.
+  { apply base_contextual_step. econstructor; simpl; done. }
+  reflexivity.
+Qed.
+
+
+(** Exercise 4 (LN Exercise 48): Fibonacci *)
+Definition knot : val :=
+  λ: "f",
+    let: "x" := new (λ: "x", #0) in
+    let: "g" := "f" (λ: "y", (! "x") "y") in
+    "x" <- "g";; "g".
+
+Definition fibonacci : val := 
+  λ: "n", knot (λ: "rec" "n",
+    if: "n" = #0 then #0 else
+    if: "n" = #1 then #1 else
+    "rec" ("n" - #1) + "rec" ("n" - #2)) "n".
+Lemma fibonacci_typed Σ n Γ :
+  TY Σ; n; Γ ⊢ fibonacci : (Int → Int).
+Proof.
+  repeat solve_typing_fast.
+Qed.
diff --git a/theories/type_systems/systemf_mu_state/logrel_sol.v b/theories/type_systems/systemf_mu_state/logrel_sol.v
new file mode 100644
index 0000000..532cf73
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/logrel_sol.v
@@ -0,0 +1,1772 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Export facts maps.
+From semantics.ts.systemf_mu_state Require Import lang notation parallel_subst execution.
+From Equations Require Export Equations.
+From Autosubst Require Export Autosubst.
+
+(** * Logical relation for SystemF + recursive types *)
+
+(** ** First-order typing for heaps *)
+(* We have to explicitly specify the type of first-order types here.
+
+  One alternative approach would be to just require first-orderness in the ref case of the logrel,
+  but this breaks the boring lemma about moving substitution: (A.[σ]) might be first-order
+  even if A is not (because it contains a type variable), so we fail to prove the equivalence.
+  Explicitly defining fotypes in this way prevents type substitution from going below Ref entirely,
+  which fixes this problem.
+*)
+
+Inductive fotype : Type :=
+  | FOInt
+  | FOBool
+  | FOUnit
+  | FOProd (A B : fotype)
+  | FOSum (A B : fotype).
+
+Inductive type : Type :=
+  (** [var] is the type of variables of Autosubst -- it unfolds to [nat] *)
+  | TVar : var → type
+  | Int
+  | Bool
+  | Unit
+  (** The [{bind 1 of type}] tells Autosubst to put a De Bruijn binder here *)
+  | TForall : {bind 1 of type} → type
+  | TExists : {bind 1 of type} → type
+  | Fun (A B : type)
+  | Prod (A B : type)
+  | Sum (A B : type)
+  | TMu : {bind 1 of type} → type
+  | Ref (a : fotype)
+.
+
+Fixpoint of_fotype (a : fotype) : type :=
+  match a with
+  | FOInt => Int
+  | FOBool => Bool
+  | FOUnit => Unit
+  | FOProd a b => Prod (of_fotype a) (of_fotype b)
+  | FOSum a b => Sum (of_fotype a) (of_fotype b)
+  end.
+Coercion of_fotype : fotype >-> type.
+
+(** Autosubst instances.
+  This lets Autosubst do its magic and derive all the substitution functions, etc.
+ *)
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+
+Definition typing_context := gmap string type.
+Implicit Types
+  (Γ : typing_context)
+  (v : val)
+  (e : expr)
+  (A B : type)
+  (* we use lower-case letters for first-order types *)
+  (a : fotype)
+.
+
+Declare Scope FType_scope.
+Delimit Scope FType_scope with ty.
+Bind Scope FType_scope with type.
+Notation "# x" := (TVar x) : FType_scope.
+Infix "→" := Fun : FType_scope.
+Notation "(→)" := Fun (only parsing) : FType_scope.
+Notation "∀: τ" :=
+  (TForall τ%ty)
+  (at level 100, τ at level 200) : FType_scope.
+Notation "∃: τ" :=
+  (TExists τ%ty)
+  (at level 100, τ at level 200) : FType_scope.
+Infix "×" := Prod (at level 70) : FType_scope.
+Notation "(×)" := Prod (only parsing) : FType_scope.
+Infix "+" := Sum : FType_scope.
+Notation "(+)" := Sum (only parsing) : FType_scope.
+Notation "μ: A" :=
+  (TMu A%ty)
+  (at level 100, A at level 200) : FType_scope.
+
+Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)) <$> Γ) (at level 10, format "⤉ Γ").
+
+Implicit Types
+  (α : var)
+.
+Inductive type_wf : nat → type → Prop :=
+  | type_wf_TVar m n:
+      m < n →
+      type_wf n (TVar m)
+  | type_wf_Int n: type_wf n Int
+  | type_wf_Bool n : type_wf n Bool
+  | type_wf_Unit n : type_wf n Unit
+  | type_wf_TForall n A :
+      type_wf (S n) A →
+      type_wf n (TForall A)
+  | type_wf_TExists n A :
+      type_wf (S n) A →
+      type_wf n (TExists A)
+  | type_wf_Fun n A B:
+      type_wf n A →
+      type_wf n B →
+      type_wf n (Fun A B)
+  | type_wf_Prod n A B :
+      type_wf n A →
+      type_wf n B →
+      type_wf n (Prod A B)
+  | type_wf_Sum n A B :
+      type_wf n A →
+      type_wf n B →
+      type_wf n (Sum A B)
+  | type_wf_mu n A :
+      type_wf (S n) A →
+      type_wf n (μ: A)
+  | type_wf_ref n a :
+      type_wf n (Ref a).
+#[export] Hint Constructors type_wf : core.
+
+Inductive bin_op_typed : bin_op → type → type → type → Prop :=
+  | plus_op_typed : bin_op_typed PlusOp Int Int Int
+  | minus_op_typed : bin_op_typed MinusOp Int Int Int
+  | mul_op_typed : bin_op_typed MultOp Int Int Int
+  | lt_op_typed : bin_op_typed LtOp Int Int Bool
+  | le_op_typed : bin_op_typed LeOp Int Int Bool
+  | eq_op_typed : bin_op_typed EqOp Int Int Bool.
+#[export] Hint Constructors bin_op_typed : core.
+
+Inductive un_op_typed : un_op → type → type → Prop :=
+  | neg_op_typed : un_op_typed NegOp Bool Bool
+  | minus_un_op_typed : un_op_typed MinusUnOp Int Int.
+
+Reserved Notation "'TY' Δ ;  Γ ⊢ e : A" (at level 74, e, A at next level).
+Inductive syn_typed : nat → typing_context → expr → type → Prop :=
+  | typed_var n Γ x A :
+      Γ !! x = Some A →
+      TY n; Γ ⊢ (Var x) : A
+  | typed_lam n Γ x e A B :
+      TY n ; (<[ x := A]> Γ) ⊢ e : B →
+      type_wf n A →
+      TY n; Γ ⊢ (Lam (BNamed x) e) : (A → B)
+  | typed_lam_anon n Γ e A B :
+      TY n ; Γ ⊢ e : B →
+      type_wf n A →
+      TY n; Γ ⊢ (Lam BAnon e) : (A → B)
+  | typed_tlam n Γ e A :
+      (* we need to shift the context up as we descend under a binder *)
+      TY S n; (⤉ Γ) ⊢ e : A →
+      TY n; Γ ⊢ (Λ, e) : (∀: A)
+  | typed_tapp n Γ A B e :
+      TY n; Γ ⊢ e : (∀: A) →
+      type_wf n B →
+      (* A.[B/] is the notation for Autosubst's substitution operation that
+        replaces variable 0 by [B] *)
+      TY n; Γ ⊢ (e <>) : (A.[B/])
+  | typed_pack n Γ A B e :
+      type_wf n B →
+      type_wf (S n) A →
+      TY n; Γ ⊢ e : (A.[B/]) →
+      TY n; Γ ⊢ (pack e) : (∃: A)
+  | typed_unpack n Γ A B e e' x :
+      type_wf n B → (* we should not leak the existential! *)
+      TY n; Γ ⊢ e : (∃: A) →
+      (* As we descend under a type variable binder for the typing of [e'],
+          we need to shift the indices in [Γ] and [B] up by one.
+        On the other hand, [A] is already defined under this binder, so we need not shift it.
+      *)
+      TY (S n); (<[x := A]>(⤉Γ)) ⊢ e' : (B.[ren (+1)]) →
+      TY n; Γ ⊢ (unpack e as BNamed x in e') : B
+  | typed_int n Γ z : TY n; Γ ⊢ (Lit $ LitInt z) : Int
+  | typed_bool n Γ b : TY n; Γ ⊢ (Lit $ LitBool b) : Bool
+  | typed_unit n Γ : TY n; Γ ⊢ (Lit $ LitUnit) : Unit
+  | typed_if n Γ e0 e1 e2 A :
+      TY n; Γ ⊢ e0 : Bool →
+      TY n; Γ ⊢ e1 : A →
+      TY n; Γ ⊢ e2 : A →
+      TY n; Γ ⊢ If e0 e1 e2 : A
+  | typed_app n Γ e1 e2 A B :
+      TY n; Γ ⊢ e1 : (A → B) →
+      TY n; Γ ⊢ e2 : A →
+      TY n; Γ ⊢ (e1 e2)%E : B
+  | typed_binop n Γ e1 e2 op A B C :
+      bin_op_typed op A B C →
+      TY n; Γ ⊢ e1 : A →
+      TY n; Γ ⊢ e2 : B →
+      TY n; Γ ⊢ BinOp op e1 e2 : C
+  | typed_unop n Γ e op A B :
+      un_op_typed op A B →
+      TY n; Γ ⊢ e : A →
+      TY n; Γ ⊢ UnOp op e : B
+  | typed_pair n Γ e1 e2 A B :
+      TY n; Γ ⊢ e1 : A →
+      TY n; Γ ⊢ e2 : B →
+      TY n; Γ ⊢ (e1, e2) : A × B
+  | typed_fst n Γ e A B :
+      TY n; Γ ⊢ e : A × B →
+      TY n; Γ ⊢ Fst e : A
+  | typed_snd n Γ e A B :
+      TY n; Γ ⊢ e : A × B →
+      TY n; Γ ⊢ Snd e : B
+  | typed_injl n Γ e A B :
+      type_wf n B →
+      TY n; Γ ⊢ e : A →
+      TY n; Γ ⊢ InjL e : A + B
+  | typed_injr n Γ e A B :
+      type_wf n A →
+      TY n; Γ ⊢ e : B →
+      TY n; Γ ⊢ InjR e : A + B
+  | typed_case n Γ e e1 e2 A B C :
+      TY n; Γ ⊢ e : B + C →
+      TY n; Γ ⊢ e1 : (B → A) →
+      TY n; Γ ⊢ e2 : (C → A) →
+      TY n; Γ ⊢ Case e e1 e2 : A
+  | typed_roll n Γ e A :
+      TY n; Γ ⊢ e : (A.[(μ: A)/]) →
+      TY n; Γ ⊢ (roll e) : (μ: A)
+  | typed_unroll n Γ e A :
+      TY n; Γ ⊢ e : (μ: A) →
+      TY n; Γ ⊢ (unroll e) : (A.[(μ: A)/])
+  (** Typing rules for state *)
+  (* We use lower-case letters, which imposes the requirement to use first-order types.
+     (The coercion [of_fotype] does a lot of work here.) *)
+  | typed_load n Γ e a :
+      TY n; Γ ⊢ e : (Ref a) →
+      TY n; Γ ⊢ !e : a
+  | typed_store n Γ e1 e2 a :
+      TY n; Γ ⊢ e1 : (Ref a) →
+      TY n; Γ ⊢ e2 : a →
+      TY n; Γ ⊢ (e1 <- e2) : Unit
+  | typed_new n Γ e a :
+      TY n; Γ ⊢ e : a →
+      TY n; Γ ⊢ (new e) : Ref a
+where "'TY'  Δ ;  Γ ⊢ e : A" := (syn_typed Δ Γ e%E A%ty).
+#[export] Hint Constructors syn_typed : core.
+
+Lemma syn_typed_closed Δ Γ e A X :
+  TY Δ; Γ ⊢ e : A →
+  (∀ x, x ∈ dom Γ → x ∈ X) →
+  is_closed X e.
+Proof.
+  induction 1 as [ | ??????? IH | | n Γ e A H IH | | | n Γ A B e e' x Hwf H1 IH1 H2 IH2 | | | | | | | | | | | | | | | | | | ] in X |-*; simpl; intros Hx; try done.
+  { (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. }
+  { (* lam *) apply IH.
+    intros y. rewrite elem_of_dom lookup_insert_is_Some.
+    intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
+    apply elem_of_cons. right. eapply Hx. by apply elem_of_dom.
+  }
+  { (* anon lam *) naive_solver. }
+  { (* tlam *)
+    eapply IH. intros x Hel. apply Hx.
+    by rewrite dom_fmap in Hel.
+  }
+  3: { (* unpack *)
+    apply andb_True; split.
+    - apply IH1. apply Hx.
+    - apply IH2. intros y. rewrite elem_of_dom lookup_insert_is_Some.
+    intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
+    apply elem_of_cons. right. eapply Hx.
+    apply elem_of_dom. revert Hy. rewrite lookup_fmap fmap_is_Some. done.
+  }
+  (* everything else *)
+  all: repeat match goal with
+              | |- Is_true (_ && _)  => apply andb_True; split
+              end.
+  all: try naive_solver.
+Qed.
+
+Goal TY 0; ∅ ⊢ (λ: "x", #1 + "x") : (Int → Int).
+Proof. eauto. Qed.
+Goal TY 0; ∅ ⊢ (Λ, λ: "x", "x") : (∀: #0 → #0).
+Proof. eauto 8. Qed.
+Goal TY 0; ∅ ⊢ (new #42 <- #1337) : Unit.
+Proof. eapply (typed_store _ _ _ _ FOInt); eauto. Qed.
+
+(** ** Worlds *)
+(** We represent heap invariants as predicates on heaps,
+  and worlds as lists of such invariants.
+ *)
+Definition heap_inv := heap → Prop.
+Definition world := list heap_inv.
+Implicit Types (W : world) (INV : heap_inv).
+(** [W'] extends [W] if [W] is a suffix of [W'] *)
+Definition wext W W' := suffix W W'.
+Notation "W' ⊒ W" := (wext W W') (at level 40).
+#[export] Instance wext_preorder : PreOrder wext.
+Proof. apply _. Qed.
+
+(** Satisfaction is defined straightforwardly by recursion.
+  We use map difference ∖ that computes the difference of two maps
+  based on the domain.
+ *)
+Fixpoint wsat W σ :=
+  match W with
+  | INV :: W' =>
+    ∃ σ0, INV σ0 ∧ σ0 ⊆ σ ∧ wsat W' (σ ∖ σ0)
+  | [] => True
+  end.
+
+Lemma wsat_mono σ σ' W :
+  σ ⊆ σ' →
+  wsat W σ → wsat W σ'.
+Proof.
+  induction W as [ | INV W' IH] in σ, σ' |-*; first done.
+  simpl. intros Hincl (σ0 & Hinv & Hincl' & Hsat).
+  exists σ0; split; first done. split; first by etrans.
+  eapply IH; last done.
+  by apply map_difference_mono.
+Qed.
+
+Lemma wsat_wext W W' σ :
+  W' ⊒ W →
+  wsat W' σ →
+  wsat W σ.
+Proof.
+  intros (L & ->). induction L as [ | INV L' IH] in σ |-*; first done.
+  simpl. intros (σ0 & Hinv & Hincl & ?%IH). eapply wsat_mono; last done.
+  by apply map_subseteq_difference_l.
+Qed.
+
+Lemma wsat_lookup W σ i P :
+  wsat W σ → W !! i = Some P →
+  ∃ σ0, σ0 ⊆ σ ∧ P σ0.
+Proof.
+  induction W as [ | INV W IH] in i, σ |-*; first done.
+  simpl. intros (σ0 & HINV & Hincl & Hsat).
+  destruct i as [ | i]; simpl.
+  - intros [= ->]. eauto.
+  - intros Hlook. destruct (IH _ _ Hsat Hlook) as (σ1 & ? & ?).
+    exists σ1; split; last done. etrans; eauto.
+    by apply map_subseteq_difference_l.
+Qed.
+
+Lemma wext_lookup W' W i INV :
+  W' ⊒ W → W !! i = Some INV → ∃ i', W' !! i' = Some INV.
+Proof.
+  unfold wext.
+  intros Hincl Hlook.
+  destruct Hincl as (W''& ->).
+  exists (length W'' + i).
+  rewrite lookup_app_r; last lia.
+  by rewrite Nat.add_comm Nat.add_sub.
+Qed.
+
+Lemma wsat_merge σ1 σ2 W1 W2 :
+  σ1 ##ₘ σ2 →
+  wsat W1 σ1 →
+  wsat W2 σ2 →
+  wsat (W1 ++ W2) (σ1 ∪ σ2).
+Proof.
+  intros Hdisj. induction W1 as [ | INV W1 IH] in W2, σ1, σ2, Hdisj |-*.
+  - simpl. intros _ Hs. eapply wsat_mono; last done. by apply map_union_subseteq_r.
+  - simpl. intros (σ0 & Hinv & Hincl & Hsat1) Hsat2.
+    exists σ0. split_and!; [ done | | ].
+    + by apply map_union_subseteq_l'.
+    + rewrite map_difference_union'; last done.
+      assert ((σ2 ∖ σ0) = σ2) as H.
+      { symmetry; apply map_disjoint_difference.
+        symmetry. eapply map_disjoint_weaken_l; done.
+      }
+      rewrite H.
+      apply IH; [ | done..].
+      eapply map_disjoint_weaken_l; first done. by apply map_subseteq_difference_l.
+Qed.
+
+(** Assuming that we have found a heap invariant [P] talking about [l] and that is invariant wrt the concrete value, we can update [l].
+ *)
+Lemma wsat_update W σ i (l : loc) (v : val) (P : heap_inv) :
+  wsat W σ → W !! i = Some P →
+  (∀ σ : heap, P σ → is_Some (σ !! l) ∧ P (<[l := v]> σ)) →
+  wsat W (<[l := v]> σ).
+Proof.
+  induction W as [ | INV W IH] in i, σ |-*; first done.
+  destruct i as [ | i].
+  - intros (σ0 & HINV & Hincl & Hsat).
+    intros [= ->] Hupd. eexists. split_and!; [eapply Hupd, HINV | | ].
+    + by apply insert_mono.
+    + apply Hupd in HINV as [[v0 Hs] _]. eapply wsat_mono; last apply Hsat.
+      rewrite (difference_insert _ _ _ _ _ v0). rewrite insert_id; done.
+  - intros Hsat Hlook Hupd.
+    destruct Hsat as (σ0 & HINV & Hincl & Hsat). simpl in *.
+    specialize (wsat_lookup _ _ _ _ Hsat Hlook) as (σ1 & Hincl' & [Hs ?]%Hupd).
+    specialize (IH _ _ Hsat Hlook Hupd).
+    assert (σ0 !! l = None) as H0l.
+    { eapply lookup_weaken_is_Some in Hincl'; last done.
+      apply lookup_difference_is_Some in Hincl'. apply Hincl'.
+    }
+    exists σ0. split_and!; [  done | | ].
+    + etrans; first by eapply (insert_subseteq _ l v).
+      by apply insert_mono.
+    + assert (<[l:=v]> σ ∖ σ0 = <[l:=v]> (σ ∖ σ0)) as ->; last done.
+      symmetry. apply insert_difference'. done.
+Qed.
+
+(** ** Definition of the logrel *)
+
+(** A semantic type consists of a value-predicate parameterized over a step-index and a world,
+   a proof of closedness, and a proof of downwards-closure wrt step-indices,
+   and a proof of upwards-closure wrt world extension.
+  *)
+Record sem_type := mk_ST {
+  sem_type_car :> nat → world → val → Prop;
+  sem_type_closed_val k W v : sem_type_car k W v → is_closed [] (of_val v);
+  sem_type_mono : ∀ k k' W v, sem_type_car k W v → k' ≤ k → sem_type_car k' W v;
+  sem_type_mono_world : ∀ k W W' v, sem_type_car k W v → W' ⊒ W → sem_type_car k W' v
+  }.
+
+(** Two tactics we will use later on.
+  [pose_sem_type P as N] defines a semantic type at name [N] with the value predicate [P].
+ *)
+(* slightly complicated formulation to make the proof term [p] opaque and prevent it from polluting the context *)
+Tactic Notation "pose_sem_type" uconstr(P) "as" ident(N) :=
+  let p := fresh "__p" in
+  let p2 := fresh "__p2" in
+  let p3 := fresh "__p3" in
+  unshelve refine ((λ p p2 p3, let N := (mk_ST P p p2 p3) in _) _ _ _); first (simpl in p, p2, p3); cycle 1.
+Tactic Notation "specialize_sem_type" constr(S) "with" uconstr(P) "as" ident(N) :=
+  pose_sem_type P as N; last specialize (S N).
+
+(** We represent type variable assignments [δ] as functions [f] into semantic types.
+  The variable [#n] (in De Bruijn representation) is mapped to [f n].
+ *)
+Definition tyvar_interp := var → sem_type.
+Implicit Types
+  (δ : tyvar_interp)
+  (τ : sem_type)
+.
+
+(**
+  In Coq, we need to make argument why the logical relation is well-defined precise:
+  (for Coq, that means: we need to show that the recursion is terminating).
+
+  To make this formal, we define a well-founded relation that allows to either decrease the step-index, the type, or switch from the expression case to the value case for recursive calls.
+  We define size measures for for all three of these things, and then combine them into a big lexicographic ordering [term_rel].
+
+  Adding in state does not provide much of a complication, _as long as we only consider first-order state_.
+  (higher-order state makes the argument quite a bit more difficult, since worlds then also need to be step-indexed).
+ *)
+Equations type_size (A : type) : nat :=
+  type_size Int := 1;
+  type_size Bool := 1;
+  type_size Unit := 1;
+  type_size (A → B) := type_size A + type_size B + 1;
+  type_size (#α) := 1;
+  type_size (∀: A) := type_size A + 2;
+  type_size (∃: A) := type_size A + 2;
+  type_size (A × B) := type_size A + type_size B + 1;
+  type_size (A + B) := max (type_size A) (type_size B) + 1;
+  type_size (μ: A) := type_size A + 2;
+  type_size (Ref A) := 2
+.
+(* [ltof A R] defines a well-founded measure on type [A] by using a mapping [R] from [A] to [nat]
+  (it lifts the < relation on natural numbers to [A]) *)
+Definition type_lt := ltof type type_size.
+#[local] Instance type_lt_wf : WellFounded type_lt.
+Proof. apply well_founded_ltof. Qed.
+
+Inductive type_case : Set :=
+  | expr_case | val_case.
+Definition type_case_size (c : type_case) : nat :=
+  match c with | expr_case => 1 | val_case => 0 end.
+Definition type_case_lt := ltof type_case type_case_size.
+#[local] Instance type_case_lt_wf : WellFounded type_case_lt.
+Proof. apply well_founded_ltof. Qed.
+
+Definition term_rel := Subterm.lexprod nat (type * type_case) lt (Subterm.lexprod type type_case type_lt type_case_lt).
+#[local] Instance term_rel_wf : WellFounded term_rel. apply _. Qed.
+
+(** *** The logical relation *)
+(** Since the relation is step-indexed now, and the argument that the case for recursive types is well-formed
+  fundamentally requires decreasing the step-index, we also need to convince Equations that this definition is well-formed!
+   We do this by providing a well-founded termination relation [term_rel] that decreases for each recursive call.
+ *)
+Equations type_interp (c : type_case) (t : type) δ (k : nat) (W : world) (v : match c with val_case => val | expr_case => expr end) : Prop
+  by wf (k, (t, c)) term_rel := {
+
+  type_interp val_case Int δ k W v =>
+    ∃ z : Z, v = #z ;
+  type_interp val_case Bool δ k W v =>
+    ∃ b : bool, v = #b ;
+  type_interp val_case Unit δ k W v =>
+    v = #LitUnit ;
+  type_interp val_case (A × B) δ k W v =>
+    ∃ v1 v2 : val, v = (v1, v2)%V ∧ type_interp val_case A δ k W v1 ∧ type_interp val_case B δ k W v2;
+  type_interp val_case (A + B) δ k W v =>
+    (∃ v' : val, v = InjLV v' ∧ type_interp val_case A δ k W v') ∨
+    (∃ v' : val, v = InjRV v' ∧ type_interp val_case B δ k W v');
+
+  type_interp val_case (A → B) δ k W v =>
+    ∃ x e, v = LamV x e ∧ is_closed (x :b: nil) e ∧
+      (* Slightly weird formulation: for down-closure, we want to quantify over all k' ≤ k --
+        but with that formulation, the termination checker will not be able to see that k' will really be smaller!
+         Thus, we quantify over the difference kd and subtract *)
+      ∀ v' kd W', W' ⊒ W →
+        type_interp val_case A δ (k - kd) W' v' →
+        type_interp expr_case B δ (k - kd) W' (subst' x (of_val v') e);
+  type_interp val_case (#α) δ k W v =>
+    (δ α).(sem_type_car) k W v;
+  type_interp val_case (∀: A) δ k W v =>
+    ∃ e, v = TLamV e ∧ is_closed [] e ∧
+      ∀ τ, type_interp expr_case A (τ .: δ) k W e;
+  type_interp val_case (∃: A) δ k W v =>
+    ∃ v', v = PackV v' ∧
+      ∃ τ : sem_type, type_interp val_case A (τ .: δ) k W v';
+  (** Defined with two cases: ordinarily, we might require [k > 0] in the body as a guard for the recursive call,
+     but this does not count as a proper guard for termination for Coq -- therefore we handle the 0-case separately.
+   *)
+  type_interp val_case (μ: A) δ (S k) W v =>
+    ∃ v', v = (roll v')%V ∧ is_closed [] v' ∧ ∀ kd, type_interp val_case (A.[μ: A/]%ty) δ (k - kd) W v';
+  type_interp val_case (μ: A) δ 0 W v =>
+    ∃ v', v = (roll v')%V ∧ is_closed [] v';
+  (** The reference case *)
+  type_interp val_case (Ref a) δ k W v =>
+      ∃ (l : loc), v = LitV $ LitLoc l ∧ ∃ i INV, W !! i = Some INV ∧
+      INV = (λ σ', ∃ v, σ' = <[ l := v ]> ∅ ∧ TY 0; ∅ ⊢ (of_val v) : a);
+
+  type_interp expr_case t δ k W e =>
+    ∀ e' h h' W' n, W' ⊒ W → wsat W' h → n < k → red_nsteps n e h e' h' → ∃ v W'', to_val e' = Some v ∧
+      W'' ⊒ W' ∧ wsat W'' h' ∧ type_interp val_case t δ (k - n) W'' v
+}.
+
+(** Proving that the arguments are decreasing for recursive calls is a bit more messy now, but it's mostly systematic.
+  Therefore we provide a simple automation tactic that will also become useful a few times below.
+*)
+Ltac dsimpl :=
+  repeat match goal with
+  | |- term_rel (?k, _) (?k, _) =>
+      (* step-index is not decreasing, go right *)
+      right
+  | |- term_rel (?k1, _) (?k2, _) =>
+      (* use [lia] to decide where to go *)
+      destruct (decide (k1 < k2)) as [ ? | ?]; [left; lia | assert (k1 = k2) as -> by lia; right]
+  | |- Subterm.lexprod type type_case _ _ (?t, _) (?t, _) =>
+      (* type is not decreasing, go right *)
+      right
+  | |- Subterm.lexprod type type_case _ _ (_, ?a) (_, ?a) =>
+      (* type case is not decreasing, go left *)
+      left
+  | |- term_rel (_, _) (_, _) =>
+      (* branch non-deterministically and try to solve the remaining goal *)
+      first [left; solve [dsimpl] | right; solve [dsimpl]]
+  | |- Subterm.lexprod type type_case  _ _ _ _ =>
+      (* branch non-deterministically *)
+      first [left; solve [dsimpl] | right; solve [dsimpl]]
+  | _ =>
+      (* try to solve a leaf, i.e. a [type_lt], [type_case_lt] or [lt] goal *)
+      unfold type_case_lt, type_lt, ltof; simp type_size; simpl; try lia
+  end.
+(** The tactic solves all of Equations' obligations for showing that the argument decreases. *)
+Solve Obligations with (intros; dsimpl).
+
+(** *** Value relation and expression relation *)
+Definition sem_val_rel A δ k W v := type_interp val_case A δ k W v.
+Definition sem_expr_rel A δ k W e := type_interp expr_case A δ k W e.
+
+Notation 𝒱 := (type_interp val_case).
+Notation ℰ := (type_interp expr_case).
+
+Lemma val_rel_is_closed v δ k W A:
+  𝒱 A δ k W v → is_closed [] (of_val v).
+Proof.
+  induction A as [ | | | | | A IHA | | A IH1 B IH2 | A IH1 B IH2 | A IHA | A] in k, v, δ |-*; simp type_interp.
+  - by eapply sem_type_closed_val.
+  - intros [z ->]. done.
+  - intros [b ->]. done.
+  - intros ->. done.
+  - intros (e & -> & ? & _). done.
+  - intros (v' & -> & (τ & Hinterp)). simpl. by eapply IHA.
+  - intros (x & e & -> & ? & _). done.
+  - intros (v1 & v2 & -> & ? & ?). simpl; apply andb_True; split; eauto.
+  - intros [(v' & -> & ?) | (v' & -> & ?)]; simpl; eauto.
+  - destruct k; simp type_interp.
+    + intros (v' & -> & ?); done.
+    + intros (v' & -> & ? & Ha); done.
+  - intros (l & -> & _). done.
+Qed.
+
+(** Downwards closure wrt step-index *)
+Lemma type_interp_mono : ∀ '(k, (A, c)) δ W k' x, k' ≤ k → type_interp c A δ k W x → type_interp c A δ k' W x.
+Proof.
+  eapply (well_founded_ind (R := term_rel) term_rel_wf).
+  intros (k & A & []) IH δ W k'.
+  { (* expression rel *)
+    intros e Hk He. simp type_interp in He. simp type_interp. intros e' h h' W' n Hincl Hsat Hn Hred.
+    destruct (He e' h h' W' n ltac:(done) ltac:(done) ltac:(lia) Hred) as (v & W'' & Hval & Hincl' & Hsat' & Hv).
+    exists v, W''. split; first done.
+    split_and!; [done.. | ].
+    eapply (IH (k-n, (A, val_case))); [ | lia | done].
+    (* show that the induction is decreasing *)
+    dsimpl.
+  }
+  intros v Hk Hv.
+  destruct A as [x | | | | A | A | A B | A B | A B | A | A ]; simp type_interp; simp type_interp in Hv.
+  - (* var case *)
+    by eapply sem_type_mono.
+  - (* universal case *)
+    destruct Hv as (e & -> & ? & Hv).
+    exists e. split_and!; [done.. | ]. intros τ.
+    eapply (IH (k, (A, expr_case))); [ dsimpl | done | done].
+  - (* existential case *)
+    destruct Hv as (v' & -> & (τ & Hv)). exists v'. split; first done.
+    exists τ. eapply (IH (k, (A, _))); [ dsimpl | done..].
+  - (* fun case *)
+    destruct Hv as (x & e & -> & ? & Hv). exists x, e. split_and!; [done..| ].
+    intros v' kd W' Hv' Hincl.
+    (* slightly tricky due to the contravariant recursive occurrence *)
+    set (kd' := k - k').
+    specialize (Hv v' (kd + kd')).
+    replace (k - (kd + kd')) with (k' - kd) in Hv by lia.
+    eapply (IH (k' - kd, (B, expr_case))); [ | lia | by eapply Hv].
+    destruct (decide (k' - kd < k)) as [ ? | ?]; first (left; lia).
+    assert (k' - kd = k) as -> by lia. dsimpl.
+  - (* pair case *)
+    destruct Hv as (v1 & v2 & -> & Hv1 & Hv2).
+    exists v1, v2. split_and!; first done.
+    all: eapply (IH (k, (_, _))); [ dsimpl | done..].
+  - (* sum case *)
+    destruct Hv as [(v' & -> & Hv) | (v' & -> & Hv)]; [ left | right].
+    all: exists v'; split; first done.
+    all: eapply (IH (k, (_, _))); [ dsimpl | done..].
+  - (* rec case *)
+    destruct k; simp type_interp in Hv.
+    { assert (k' = 0) as -> by lia. simp type_interp. }
+    destruct Hv as (v' & -> & ? & Hv).
+    destruct k' as [ | k']; simp type_interp.
+    { eauto. }
+    exists v'. split_and!; [ done.. | ].
+    intros kd.
+    (* here we crucially use that we can decrease the index *)
+    eapply (IH (k - kd, (A.[(μ: A)%ty/], val_case))); [ | lia | done].
+    left. lia.
+Qed.
+
+(** We can now derive the two desired lemmas *)
+Lemma val_rel_mono_idx A δ k k' W v : k' ≤ k → 𝒱 A δ k W v → 𝒱 A δ k' W v.
+Proof. apply (type_interp_mono (k, (A, val_case))). Qed.
+Lemma expr_rel_mono_idx A δ k k' W e : k' ≤ k → ℰ A δ k W e → ℰ A δ k' W e.
+Proof. apply (type_interp_mono (k, (A, expr_case))). Qed.
+
+(** Up-closure wrt worlds *)
+Lemma type_interp_mono_world : ∀ '(k, (A, c)) δ W W' x, W' ⊒ W → type_interp c A δ k W x → type_interp c A δ k W' x.
+Proof.
+  eapply (well_founded_ind (R := term_rel) term_rel_wf).
+  intros (k & A & []) IH δ W W'.
+  { (* expression rel *)
+    intros e HW He. simp type_interp in He. simp type_interp. intros e' h h' W'' n Hincl Hsat Hn Hred.
+    destruct (He e' h h' W'' n ltac:(etrans; done) ltac:(done) ltac:(lia) Hred) as (v & W''' & Hval & Hincl' & Hsat' & Hv).
+    exists v, W'''. split; first done.
+    split_and!; [done.. | ].
+    eapply (IH (k-n, (A, val_case))); [ |  | apply Hv].
+    - dsimpl.
+    - done.
+  }
+  intros v HW Hv.
+  destruct A as [x | | | | A | A | A B | A B | A B | A | A ]; simp type_interp; simp type_interp in Hv.
+  - (* var case *)
+    by eapply sem_type_mono_world.
+  - (* universal case *)
+    destruct Hv as (e & -> & ? & Hv).
+    exists e. split_and!; [done.. | ]. intros τ.
+    eapply (IH (k, (A, expr_case))); [ dsimpl | done | done].
+  - (* existential case *)
+    destruct Hv as (v' & -> & (τ & Hv)). exists v'. split; first done.
+    exists τ. eapply (IH (k, (A, _))); [ dsimpl | done..].
+  - (* fun case *)
+    destruct Hv as (x & e & -> & ? & Hv). exists x, e. split_and!; [done..| ].
+    intros v' kd W'' Hincl Hv'.
+    specialize (Hv v' kd W'').
+    eapply (IH (k - kd, (B, expr_case))); [ dsimpl | | eapply Hv].
+    + done.
+    + etrans; done.
+    + eapply (IH (k -kd, (A, val_case))); last done; last done. dsimpl.
+  - (* pair case *)
+    destruct Hv as (v1 & v2 & -> & Hv1 & Hv2).
+    exists v1, v2. split_and!; first done.
+    all: eapply (IH (k, (_, _))); [ dsimpl | done..].
+  - (* sum case *)
+    destruct Hv as [(v' & -> & Hv) | (v' & -> & Hv)]; [ left | right].
+    all: exists v'; split; first done.
+    all: eapply (IH (k, (_, _))); [ dsimpl | done..].
+  - (* rec case *)
+    destruct k; simp type_interp in Hv.
+    { simp type_interp. }
+    destruct Hv as (v' & -> & ? & Hv).
+    simp type_interp.
+    exists v'. split_and!; [ done.. | ].
+    intros kd.
+    (* here we crucially use that we can decrease the index *)
+    eapply (IH (k - kd, (A.[(μ: A)%ty/], val_case))); [ | done | done].
+    left. lia.
+  - (* loc case *)
+    destruct Hv as (l & -> & (i & INV & Hlook & Heq)).
+    exists l. split; first done.
+    destruct (wext_lookup _ _ _ _ HW Hlook) as (i' & Hlook').
+    exists i', INV. done.
+Qed.
+
+Lemma val_rel_mono_world A δ k W W' v : W' ⊒ W → 𝒱 A δ k W v → 𝒱 A δ k W' v.
+Proof. apply (type_interp_mono_world (k, (A, val_case))). Qed.
+Lemma expr_rel_mono_world A δ k W W' e : W' ⊒ W → ℰ A δ k W e → ℰ A δ k W' e.
+Proof. apply (type_interp_mono_world (k, (A, expr_case))). Qed.
+
+Lemma val_rel_mono A δ k k' W W' v : k' ≤ k → W' ⊒ W → 𝒱 A δ k W v → 𝒱 A δ k' W' v.
+Proof.
+  intros. eapply val_rel_mono_idx; last eapply val_rel_mono_world; done.
+Qed.
+Lemma expr_rel_mono A δ k k' W W' e : k' ≤ k → W' ⊒ W → ℰ A δ k W e → ℰ A δ k' W' e.
+Proof.
+  intros. eapply expr_rel_mono_idx; last eapply expr_rel_mono_world; done.
+Qed.
+
+(** This is the Value Inclusion lemma from the lecture notes *)
+Lemma sem_val_expr_rel A δ k W v :
+  𝒱 A δ k W v → ℰ A δ k W (of_val v).
+Proof.
+  simp type_interp. intros Hv e' h h' W' n Hincl HW Hn (-> & -> & ->)%nsteps_val_inv.
+  rewrite to_of_val. eexists _, W'; split; first done.
+  replace (k - 0) with k by lia.
+  split_and!; [done | done | ].
+  by eapply val_rel_mono_world.
+Qed.
+
+Lemma sem_expr_rel_zero_trivial A δ W e :
+  ℰ A δ 0 W e.
+Proof.
+  simp type_interp. intros ???. lia.
+Qed.
+
+(** Interpret a syntactic type *)
+Program Definition interp_type A δ : sem_type := {|
+  sem_type_car := 𝒱 A δ;
+|}.
+Next Obligation. by eapply val_rel_is_closed. Qed.
+Next Obligation. by eapply val_rel_mono. Qed.
+Next Obligation. by eapply val_rel_mono_world. Qed.
+
+(** Semantic typing of contexts *)
+Implicit Types
+  (θ : gmap string expr).
+
+(** Context relation *)
+Inductive sem_context_rel (δ : tyvar_interp) (k : nat) (W : world) : typing_context → (gmap string expr) → Prop :=
+  | sem_context_rel_empty : sem_context_rel δ k W ∅ ∅
+  | sem_context_rel_insert Γ θ v x A :
+    𝒱 A δ k W v →
+    sem_context_rel δ k W Γ θ →
+    sem_context_rel δ k W (<[x := A]> Γ) (<[x := of_val v]> θ).
+
+Notation 𝒢 := sem_context_rel.
+
+Lemma sem_context_rel_vals {δ k W Γ θ x A} :
+  sem_context_rel δ k W Γ θ →
+  Γ !! x = Some A →
+  ∃ e v, θ !! x = Some e ∧ to_val e = Some v ∧ 𝒱 A δ k W v.
+Proof.
+  induction 1 as [|Γ θ v y B Hvals Hctx IH].
+  - naive_solver.
+  - rewrite lookup_insert_Some. intros [[-> ->]|[Hne Hlook]].
+    + do 2 eexists. split; first by rewrite lookup_insert.
+      split; first by eapply to_of_val. done.
+    + eapply IH in Hlook as (e & w & Hlook & He & Hval).
+      do 2 eexists; split; first by rewrite lookup_insert_ne.
+      split; first done. done.
+Qed.
+
+Lemma sem_context_rel_subset δ k W Γ θ :
+  𝒢 δ k W Γ θ → dom Γ ⊆ dom θ.
+Proof.
+  intros Hctx. apply elem_of_subseteq. intros x (A & Hlook)%elem_of_dom.
+  eapply sem_context_rel_vals in Hlook as (e & v & Hlook & Heq & Hval); last done.
+  eapply elem_of_dom; eauto.
+Qed.
+
+Lemma sem_context_rel_dom_eq δ k W Γ θ :
+  𝒢 δ k W Γ θ → dom Γ = dom θ.
+Proof.
+  induction 1 as [ | ??????? IH].
+  - rewrite !dom_empty //.
+  - rewrite !dom_insert IH //.
+Qed.
+
+Lemma sem_context_rel_closed δ k W Γ θ:
+  𝒢 δ k W Γ θ → subst_is_closed [] θ.
+Proof.
+  induction 1 as [ | Γ θ v x A Hv Hctx IH]; rewrite /subst_is_closed.
+  - naive_solver.
+  - intros y e. rewrite lookup_insert_Some.
+    intros [[-> <-]|[Hne Hlook]].
+    + by eapply val_rel_is_closed.
+    + eapply IH; last done.
+Qed.
+
+Lemma sem_context_rel_mono_idx Γ δ k k' W θ :
+  k' ≤ k → 𝒢 δ k W Γ θ → 𝒢 δ k' W Γ θ.
+Proof.
+  intros Hk. induction 1 as [|Γ θ v y B Hvals Hctx IH]; constructor.
+  - eapply val_rel_mono_idx; done.
+  - apply IH.
+Qed.
+Lemma sem_context_rel_mono_world Γ δ k W W' θ :
+  W' ⊒ W → 𝒢 δ k W Γ θ → 𝒢 δ k W' Γ θ.
+Proof.
+  intros HW. induction 1 as [|Γ θ v y B Hvals Hctx IH]; constructor.
+  - eapply val_rel_mono_world; done.
+  - apply IH.
+Qed.
+Lemma sem_context_rel_mono Γ δ k k' W W' θ :
+  k' ≤ k → W' ⊒ W → 𝒢 δ k W Γ θ → 𝒢 δ k' W' Γ θ.
+Proof.
+  intros. eapply sem_context_rel_mono_idx; last eapply sem_context_rel_mono_world; done.
+Qed.
+
+(** *** Semantic typing judgment *)
+Definition sem_typed (Δ : nat) Γ e A :=
+  ∀ θ δ k W, 𝒢 δ k W Γ θ → ℰ A δ k W (subst_map θ e).
+Notation "'TY' Δ ;  Γ ⊨ e : A" := (sem_typed Δ Γ e A) (at level 74, e, A at next level).
+
+Section boring_lemmas.
+  (** The lemmas in this section are all quite boring and expected statements,
+    but are quite technical to prove due to De Bruijn binders.
+    We encourage to skip over the proofs of these lemmas.
+  *)
+
+  Lemma type_interp_ext  :
+    ∀ '(k, (B, c)), ∀ δ δ' W x,
+    (∀ n k v W', W' ⊒ W → δ n k W' v ↔ δ' n k W' v) →
+    type_interp c B δ k W x ↔ type_interp c B δ' k W x.
+  Proof.
+    eapply (well_founded_ind (R := term_rel) term_rel_wf).
+    intros (k & A & []) IH δ δ'.
+    { (* expression rel *)
+      intros W e Hd. simp type_interp. eapply forall_proper; intros e'.
+      eapply forall_proper; intros h. eapply forall_proper; intros h'.
+      eapply forall_proper; intros W'. eapply forall_proper; intros n.
+      eapply if_iff'; intros. eapply if_iff'; intros _. eapply if_iff'; intros _.
+      eapply if_iff; first done. f_equiv. intros v. f_equiv. intros W''.
+      f_equiv. apply and_iff'; intros. f_equiv.
+      eapply (IH ((k - n), (A, val_case))); first dsimpl.
+      intros; apply Hd. etrans; last etrans; done.
+    }
+    intros W v Hd. destruct A as [x | | | | A | A | A B | A B | A B | A | A ]; simp type_interp; eauto.
+    - apply Hd. done.
+    - f_equiv; intros e. f_equiv. f_equiv.
+      eapply forall_proper; intros τ.
+      eapply (IH (_, (_, _))); first dsimpl.
+      intros [|m] ?; simpl; eauto.
+    - f_equiv; intros w. f_equiv. f_equiv. intros τ.
+      eapply (IH (_, (_, _))); first dsimpl.
+      intros [|m] ?; simpl; eauto.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv. eapply forall_proper. intros ?.
+      eapply forall_proper. intros ?.
+      eapply forall_proper. intros W'.
+      eapply if_iff'; intros.
+      eapply if_iff; (eapply (IH (_, (_, _))); first dsimpl).
+      all: intros; eapply Hd; etrans; done.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
+    - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
+    - destruct k; simp type_interp.
+      + done.
+      + f_equiv; intros ?. f_equiv. f_equiv.
+        eapply forall_proper; intros ?.
+        by eapply (IH (_, (_, _))); first dsimpl.
+  Qed.
+
+  Lemma type_interp_move_ren :
+    ∀ '(k, (B, c)), ∀ δ W σ x, type_interp c B (λ n, δ (σ n)) k W x ↔ type_interp c (rename σ B) δ k W x.
+  Proof.
+    eapply (well_founded_ind (R := term_rel) term_rel_wf).
+    intros (k & A & []) IH δ W σ.
+    { (* expression rel *)
+      intros e. simp type_interp. eapply forall_proper; intros e'.
+      eapply forall_proper; intros h. eapply forall_proper; intros h'.
+      eapply forall_proper; intros W'. eapply forall_proper; intros n.
+
+      eapply if_iff; first done. eapply if_iff; first done.
+      eapply if_iff; first done. eapply if_iff; first done.
+      f_equiv. intros v. f_equiv. intros W''. f_equiv. f_equiv. f_equiv.
+      eapply (IH (_, (_, _))).
+      (* show that the induction is decreasing *)
+      dsimpl.
+    }
+    intros v. destruct A as [x | | | | A | A | A B | A B | A B | A | A ]; simpl; simp type_interp; eauto.
+    - f_equiv; intros e. f_equiv. f_equiv.
+      eapply forall_proper; intros τ.
+      etransitivity; last eapply (IH (_, (_, _))); last dsimpl.
+      eapply (type_interp_ext (_, (_, _))).
+      intros [|m] ?; simpl; eauto.
+    - f_equiv; intros w. f_equiv. f_equiv. intros τ.
+      etransitivity; last eapply (IH (_, (_, _))); last dsimpl.
+      eapply (type_interp_ext (_, (_, _))).
+      intros [|m] ?; simpl; eauto.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv. eapply forall_proper. intros ?.
+      eapply forall_proper. intros ?. eapply forall_proper. intros ?.
+      eapply if_iff; first done. eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
+    - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
+    - destruct k; simp type_interp.
+      + done.
+      + f_equiv; intros ?. f_equiv. f_equiv.
+        eapply forall_proper; intros ?.
+        etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
+        asimpl. done.
+  Qed.
+
+  Lemma type_interp_move_subst  :
+    ∀ '(k, (B, c)), ∀ δ W σ x, type_interp c B (λ n, interp_type (σ n) δ) k W x ↔ type_interp c (B.[σ]) δ k W x.
+  Proof.
+    eapply (well_founded_ind (R := term_rel) term_rel_wf).
+    intros (k & A & []) IH δ W σ.
+    { (* expression rel *)
+      intros e. simp type_interp. eapply forall_proper; intros e'.
+      eapply forall_proper; intros h. eapply forall_proper; intros h'.
+      eapply forall_proper; intros W'. eapply forall_proper; intros n.
+
+      eapply if_iff; first done. eapply if_iff; first done.
+      eapply if_iff; first done. eapply if_iff; first done.
+      f_equiv. intros v. f_equiv. intros W''. f_equiv. f_equiv. f_equiv.
+      eapply (IH (_, (_, _))).
+      (* show that the induction is decreasing *)
+      dsimpl.
+    }
+    intros v. destruct A as [x | | | | A | A | A B | A B | A B | A | A]; simpl; simp type_interp; eauto.
+    - f_equiv; intros e. f_equiv. f_equiv.
+      eapply forall_proper; intros τ.
+      etransitivity; last eapply (IH (_, (_, _))); last dsimpl.
+      eapply (type_interp_ext (_, (_, _))).
+      intros [|m] ??? ?; simpl.
+      + asimpl. simp type_interp. done.
+      + unfold up; simpl. etransitivity;
+          last eapply (type_interp_move_ren (_, (_, _))).
+        done.
+    - f_equiv; intros w. f_equiv. f_equiv. intros τ.
+      etransitivity; last eapply (IH (_, (_, _))); last dsimpl.
+      eapply (type_interp_ext (_, (_, _))).
+      intros [|m] ? ???; simpl.
+      + asimpl. simp type_interp. done.
+      + unfold up; simpl. etransitivity;
+          last eapply (type_interp_move_ren (_, (_, _))).
+        done.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv. eapply forall_proper. intros ?.
+      eapply forall_proper. intros ?. eapply forall_proper. intros W'.
+      eapply if_iff; first done.
+      eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
+    - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
+    - destruct k; simp type_interp.
+      + done.
+      + f_equiv; intros ?. f_equiv. f_equiv.
+        eapply forall_proper; intros ?.
+        etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
+        asimpl. done.
+  Qed.
+
+
+  Lemma sem_val_rel_move_single_subst A B δ k v W :
+    𝒱 B (interp_type A δ .: δ) k W v ↔ 𝒱 (B.[A/]) δ k W v.
+  Proof.
+    etransitivity; last eapply (type_interp_move_subst (_, (_, _))).
+    eapply (type_interp_ext (_, (_, _))).
+    intros [| n] ? w W' ?; simpl; simp type_interp; done.
+  Qed.
+
+  Lemma sem_expr_rel_move_single_subst A B δ k W e :
+    ℰ B (interp_type A δ .: δ) k W e ↔ ℰ (B.[A/]) δ k W e.
+  Proof.
+    etransitivity; last eapply (type_interp_move_subst (_, (_, _))).
+    eapply (type_interp_ext (_, (_, _))).
+    intros [| n] ? w W' ?; simpl; simp type_interp; done.
+  Qed.
+
+  Lemma sem_val_rel_cons A δ k v W τ :
+    𝒱 A δ k W v ↔ 𝒱 A.[ren (+1)] (τ .: δ) k W v.
+  Proof.
+    etransitivity; last eapply (type_interp_move_subst (_, (_, _))).
+    eapply (type_interp_ext (_, (_, _))).
+    intros [| n] ? w W' ?; simpl; simp type_interp; done.
+  Qed.
+
+  Lemma sem_expr_rel_cons A δ k e W τ :
+    ℰ A δ k W e ↔ ℰ A.[ren (+1)] (τ .: δ) k W e.
+  Proof.
+    etransitivity; last eapply (type_interp_move_subst (_, (_, _))).
+    eapply (type_interp_ext (_, (_, _))).
+    intros [| n] ? w W' ?; simpl; simp type_interp; done.
+  Qed.
+
+  Lemma sem_context_rel_cons Γ k δ θ τ W :
+    𝒢 δ k W Γ θ →
+    𝒢 (τ .: δ) k W (⤉ Γ) θ.
+  Proof.
+    induction 1 as [ | Γ θ v x A Hv Hctx IH]; simpl.
+    - rewrite fmap_empty. constructor.
+    - rewrite fmap_insert. constructor; last done.
+      rewrite -sem_val_rel_cons. done.
+  Qed.
+End boring_lemmas.
+
+(** Bind lemma *)
+Lemma bind K e k W δ A B :
+  ℰ A δ k W e →
+  (∀ j v W', j ≤ k → W' ⊒ W → 𝒱 A δ j W' v → ℰ B δ j W' (fill K (of_val v))) →
+  ℰ B δ k W (fill K e).
+Proof.
+  intros H1 H2. simp type_interp in H1. simp type_interp.
+  intros e' h h' W' n HW Hsat Hn (j & e'' & h'' & Hj & Hred1 & Hred2)%red_nsteps_fill.
+  specialize (H1 e'' h h'' W' j ltac:(done) ltac:(done) ltac:(lia) Hred1) as (v & W'' & Hev & Hincl' & Hsat' & Hv).
+  specialize (H2 (k-j) v W'' ltac:(lia) ltac:(etrans; done) Hv).
+  simp type_interp in H2.
+  rewrite (of_to_val _ _ Hev) in H2.
+  eapply H2 in Hred2; cycle 1; [ reflexivity | done | lia | ].
+  assert (k - n = k - j - (n - j)) as -> by lia.
+  destruct Hred2 as (v' & W''' & ? & ? & ? & Hred2).
+  exists v', W'''. split_and!; [done | | done | done].
+  etrans; done.
+Qed.
+
+(** This is the closure-under-expansion lemma from the lecture notes *)
+Lemma expr_det_step_closure e e' A δ k W :
+  det_step e e' →
+  ℰ A δ (k - 1) W e' →
+  ℰ A δ k W e.
+Proof.
+  simp type_interp. intros Hdet Hexpr e'' h h' W' n Hincl Hsat Hn [? Hred]%(det_step_red _ e'); last done.
+  destruct (Hexpr e'' h h' W' (n -1) Hincl Hsat ) as (v & W'' & Hev & Hincl' & Hsat' & Hv); [lia | done | ].
+  exists v, W''. split; first done. split; first done.
+  replace (k - n) with (k - 1 - (n - 1)) by lia. done.
+Qed.
+
+Lemma expr_det_steps_closure e e' A δ k W n :
+  nsteps det_step n e e' → ℰ A δ (k - n) W e' → ℰ A δ k W e.
+Proof.
+  induction 1 as [ | n e1 e2 e3 Hstep Hsteps IH] in k |-* .
+  - replace (k - 0) with k by lia. done.
+  - intros He.
+    eapply expr_det_step_closure; first done.
+    apply IH. replace (k - 1 - n) with (k - (S n)) by lia. done.
+Qed.
+
+(** ** Compatibility lemmas *)
+
+Lemma compat_int Δ Γ z : TY Δ; Γ ⊨ (Lit $ LitInt z) : Int.
+Proof.
+  intros θ δ k W _.
+  eapply (sem_val_expr_rel _ _ _ _ #z).
+  simp type_interp. eauto.
+Qed.
+
+Lemma compat_bool Δ Γ b : TY Δ; Γ ⊨ (Lit $ LitBool b) : Bool.
+Proof.
+  intros θ δ k W _.
+  eapply (sem_val_expr_rel _ _ _ _ #b). simp type_interp. eauto.
+Qed.
+
+Lemma compat_unit Δ Γ : TY Δ; Γ ⊨ (Lit $ LitUnit) : Unit.
+Proof.
+  intros θ δ k W _.
+  eapply (sem_val_expr_rel _ _ _ _ #LitUnit).
+  simp type_interp. eauto.
+Qed.
+
+Lemma compat_var Δ Γ x A :
+  Γ !! x = Some A →
+  TY Δ; Γ ⊨ (Var x) : A.
+Proof.
+  intros Hx θ δ k W Hctx; simpl.
+  specialize (sem_context_rel_vals Hctx Hx) as (e & v & He & Heq & Hv).
+  rewrite He. simp type_interp.
+  rewrite -(of_to_val _ _ Heq).
+  intros e' h h' W' n Hincl Hsat Hn (-> & -> & ->)%nsteps_val_inv.
+  rewrite to_of_val. eexists _, _.
+  split_and!; [done.. | ].
+  replace (k -0) with k by lia.
+  eapply val_rel_mono_world; done.
+Qed.
+
+Lemma compat_app Δ Γ e1 e2 A B :
+  TY Δ; Γ ⊨ e1 : (A → B) →
+  TY Δ; Γ ⊨ e2 : A →
+  TY Δ; Γ ⊨ (e1 e2) : B.
+Proof.
+  intros Hfun Harg θ δ k W Hctx; simpl.
+  specialize (Hfun _ _ _ _ Hctx).
+  specialize (Harg _ _ _ _ Hctx).
+
+  eapply (bind [AppRCtx _]); first done.
+  intros j v W' Hj HW Hv. simpl.
+
+  eapply (bind [AppLCtx _ ]).
+  { eapply expr_rel_mono; cycle -1; [done | lia | done]. }
+  intros j' f W'' Hj' HW' Hf.
+
+  simp type_interp in Hf. destruct Hf as (x & e & -> & Hcl & Hf).
+  specialize (Hf v 0).
+  replace (j' - 0) with j' in Hf by lia.
+  eapply expr_det_step_closure.
+  { eapply det_step_beta. apply is_val_of_val. }
+  eapply expr_rel_mono_idx; last apply Hf; [lia | reflexivity | ].
+  eapply val_rel_mono; last done; [lia | done].
+Qed.
+
+Lemma is_closed_subst_map_delete X Γ (x: string) θ A e:
+  closed X e →
+  subst_is_closed [] θ →
+  dom Γ ⊆ dom θ →
+  (∀ y : string, y ∈ X → y ∈ dom (<[x:=A]> Γ)) →
+  is_closed (x :b: []) (subst_map (delete x θ) e).
+Proof.
+  intros He Hθ Hdom1 Hdom2.
+  eapply closed_subst_weaken; [ | | apply He].
+  - eapply subst_is_closed_subseteq; last done.
+    apply map_delete_subseteq.
+  - intros y Hy%Hdom2 Hn. apply elem_of_list_singleton.
+    apply not_elem_of_dom in Hn. apply elem_of_dom in Hy.
+    destruct (decide (x = y)) as [<- | Hneq]; first done.
+    rewrite lookup_delete_ne in Hn; last done.
+    rewrite lookup_insert_ne in Hy; last done.
+    move: Hdom1. rewrite elem_of_subseteq.
+    move : Hn Hy. rewrite -elem_of_dom -not_elem_of_dom.
+    naive_solver.
+Qed.
+
+(** Lambdas need to be closed by the context *)
+Lemma compat_lam_named Δ Γ x e A B X :
+  closed X e →
+  (∀ y, y ∈ X → y ∈ dom (<[x := A]> Γ)) →
+  TY Δ; (<[ x := A ]> Γ) ⊨ e : B →
+  TY Δ; Γ ⊨ (Lam (BNamed x) e) : (A → B).
+Proof.
+  intros Hcl Hsub Hbody θ δ k W Hctxt. simpl.
+  eapply (sem_val_expr_rel _ _ _ _ (LamV x _)).
+  simp type_interp.
+  eexists (BNamed x), _. split_and!; [done| | ].
+  { eapply is_closed_subst_map_delete; eauto.
+    + eapply sem_context_rel_closed in Hctxt. naive_solver.
+    + eapply sem_context_rel_subset in Hctxt; naive_solver.
+  }
+
+  intros v' kd W' Hv' Hincl.
+  specialize (Hbody (<[ x := of_val v']> θ) δ (k - kd) W').
+  simpl. rewrite subst_subst_map.
+  2: { by eapply sem_context_rel_closed. }
+  apply Hbody.
+  apply sem_context_rel_insert; first done.
+  eapply sem_context_rel_mono; [| done| done]. lia.
+Qed.
+
+Lemma is_closed_subst_map_anon X Γ θ e:
+  closed X e →
+  subst_is_closed [] θ →
+  dom Γ ⊆ dom θ →
+  (∀ y, y ∈ X → y ∈ dom Γ) →
+  is_closed [] (subst_map θ e).
+Proof.
+  intros He Hθ Hdom1 Hdom2.
+  eapply closed_subst_weaken; [ | | apply He].
+  - eapply subst_is_closed_subseteq; done.
+  - intros y Hy%Hdom2 Hn.
+    apply not_elem_of_dom in Hn. apply elem_of_dom in Hy.
+    move: Hdom1. rewrite elem_of_subseteq.
+    move : Hn Hy. rewrite -elem_of_dom -not_elem_of_dom.
+    naive_solver.
+Qed.
+
+Lemma compat_lam_anon Δ Γ e A B X :
+  closed X e →
+  (∀ y, y ∈ X → y ∈ dom Γ) →
+  TY Δ; Γ ⊨ e : B →
+  TY Δ; Γ ⊨ (Lam BAnon e) : (A → B).
+Proof.
+  intros Hcl Hsub Hbody θ δ k W Hctxt. simpl.
+  eapply (sem_val_expr_rel _ _ _ _ (LamV BAnon _)).
+  simp type_interp.
+  eexists BAnon, _. split_and!; [done| | ].
+  { eapply is_closed_subst_map_anon; eauto.
+    + eapply sem_context_rel_closed in Hctxt. naive_solver.
+    + eapply sem_context_rel_subset in Hctxt; naive_solver.
+  }
+
+  intros v' kd W' Hv' Hincl.
+  apply (Hbody θ δ (k - kd) W').
+  eapply sem_context_rel_mono; [ | done..]. lia.
+Qed.
+
+Lemma compat_int_binop Δ Γ op e1 e2 :
+  bin_op_typed op Int Int Int →
+  TY Δ; Γ ⊨ e1 : Int →
+  TY Δ; Γ ⊨ e2 : Int →
+  TY Δ; Γ ⊨ (BinOp op e1 e2) : Int.
+Proof.
+  intros Hop He1 He2 θ δ k W Hctx. simpl.
+  specialize (He1 _ _ _ _ Hctx).
+  specialize (He2 _ _ _ _ Hctx).
+
+  eapply (bind [BinOpRCtx _ _]); first done.
+  intros j v2 W' Hj HW Hv2. simpl.
+
+  eapply (bind [BinOpLCtx _ _ ]).
+  { eapply expr_rel_mono; last done; [lia | done]. }
+  intros j' v1 W'' Hj' HW' Hv1.
+
+  simp type_interp. intros e' h h' W''' n Hincl' Hsat' Hn Hred.
+  simp type_interp in Hv1. simp type_interp in Hv2.
+  destruct Hv1 as (z1 & ->). destruct Hv2 as (z2 & ->).
+
+  inversion Hop; subst; simpl.
+  all: eapply det_step_red in Hred as [ ? Hred]; [ |  eapply det_step_binop; done].
+  all: apply nsteps_val_inv in Hred as (? & -> & ->).
+  all: eexists _, W'''; simpl; split_and!; [done.. | ].
+  all: simp type_interp; eauto.
+Qed.
+
+Lemma compat_int_bool_binop Δ Γ op e1 e2 :
+  bin_op_typed op Int Int Bool →
+  TY Δ; Γ ⊨ e1 : Int →
+  TY Δ; Γ ⊨ e2 : Int →
+  TY Δ; Γ ⊨ (BinOp op e1 e2) : Bool.
+Proof.
+  intros Hop He1 He2 θ δ k W Hctx. simpl.
+  specialize (He1 _ _ _ _ Hctx).
+  specialize (He2 _ _ _ _ Hctx).
+
+  eapply (bind [BinOpRCtx _ _]); first done.
+  intros j v2 W' Hj HW Hv2. simpl.
+
+  eapply (bind [BinOpLCtx _ _ ]).
+  { eapply expr_rel_mono; last done; [lia | done]. }
+  intros j' v1 W'' Hj' HW' Hv1.
+
+  simp type_interp. intros e' h h' W''' n Hincl' Hsat' Hn Hred.
+  simp type_interp in Hv1. simp type_interp in Hv2.
+  destruct Hv1 as (z1 & ->). destruct Hv2 as (z2 & ->).
+
+  inversion Hop; subst; simpl.
+  all: eapply det_step_red in Hred as [ ? Hred]; [ |  eapply det_step_binop; done].
+  all: apply nsteps_val_inv in Hred as (? & -> & ->).
+  all: eexists _, _; simpl; split_and!; [done.. | ].
+  all: simp type_interp; eauto.
+Qed.
+
+Lemma compat_unop Δ Γ op A B e :
+  un_op_typed op A B →
+  TY Δ; Γ ⊨ e : A →
+  TY Δ; Γ ⊨ (UnOp op e) : B.
+Proof.
+  intros Hop He θ δ k W Hctx. simpl.
+  specialize (He _ _ _ _ Hctx).
+
+  eapply (bind [UnOpCtx _]); first done.
+  intros j v W' Hj HW' Hv. simpl.
+
+  simp type_interp. intros e' h h' W'' n HWincl' Hsat' Hn Hred.
+  inversion Hop; subst.
+  all: simp type_interp in Hv; destruct Hv as (? & ->).
+  all: eapply det_step_red in Hred as [ ? Hred]; [ |  eapply det_step_unop; done].
+  all: apply nsteps_val_inv in Hred as (? & -> & ->).
+  all: eexists _, _; simpl; split_and!; [done.. | ].
+  all: simp type_interp; eauto.
+Qed.
+
+Lemma compat_tlam Δ Γ e A X :
+  closed X e →
+  (∀ y, y ∈ X → y ∈ dom Γ) →
+  TY S Δ; (⤉ Γ) ⊨ e : A →
+  TY Δ; Γ ⊨ (Λ, e) : (∀: A).
+Proof.
+  intros Hcl Hsub He θ δ k W Hctx. simpl.
+  simp type_interp.
+  intros e' h h' W' n HW Hsat' Hn Hred. eapply nsteps_val_inv' in Hred as ( -> & -> & ->); last done.
+  eexists _, _; split_and!; [done..| ].
+  simp type_interp.
+  eexists _. split_and!; [ done | | ].
+  { eapply is_closed_subst_map_anon; eauto.
+    + eapply sem_context_rel_closed in Hctx; naive_solver.
+    + eapply sem_context_rel_subset in Hctx; naive_solver.
+  }
+  intros τ. eapply He.
+  replace (k -0) with k by lia. eapply sem_context_rel_cons.
+  eapply sem_context_rel_mono_world; done.
+Qed.
+
+Lemma compat_tapp Δ Γ e A B :
+  type_wf Δ B →
+  TY Δ; Γ ⊨ e : (∀: A) →
+  TY Δ; Γ ⊨ (e <>) : (A.[B/]).
+Proof.
+  intros Hwf He θ δ k W Hctx. simpl.
+
+  specialize (He _ _ _ _ Hctx).
+  eapply (bind [TAppCtx]); first done.
+  intros j v W' Hj HW Hv.
+  simp type_interp in Hv.
+  destruct Hv as (e' & -> & ? & He').
+
+  set (τ := interp_type B δ).
+  specialize (He' τ). simpl.
+  eapply expr_det_step_closure.
+  { apply det_step_tbeta. }
+  eapply sem_expr_rel_move_single_subst.
+  eapply expr_rel_mono_idx; last done.
+  lia.
+Qed.
+
+Lemma compat_pack Γ e n A B :
+  type_wf n B →
+  type_wf (S n) A →
+  TY n; Γ ⊨ e : A.[B/] →
+  TY n; Γ ⊨ (pack e) : (∃: A).
+Proof.
+  intros Hwf Hwf' He θ δ k W Hctx. simpl.
+
+  specialize (He _ _ _ _ Hctx).
+  eapply (bind [PackCtx]); first done.
+  intros j v W' Hj HW Hv.
+  simpl. eapply (sem_val_expr_rel _ _ _ _ (PackV v)).
+  simp type_interp. exists v; split; first done.
+  exists (interp_type B δ).
+  apply sem_val_rel_move_single_subst. done.
+Qed.
+
+Lemma compat_unpack n Γ A B e e' x :
+  type_wf n B →
+  TY n; Γ ⊨ e : (∃: A) →
+  TY S n; <[x:=A]> (⤉Γ) ⊨ e' : B.[ren (+1)] →
+  TY n; Γ ⊨ (unpack e as BNamed x in e') : B.
+Proof.
+  intros Hwf He He' θ δ k W Hctx. simpl.
+
+  specialize (He _ _ _ _ Hctx).
+  eapply (bind [UnpackCtx _ _]); first done.
+  intros j v W' Hj HW Hv.
+  simp type_interp in Hv. destruct Hv as (v' & -> & τ & Hv').
+  simpl.
+
+  eapply expr_det_step_closure.
+  { apply det_step_unpack. apply is_val_of_val. }
+  simpl. rewrite subst_subst_map; last by eapply sem_context_rel_closed.
+
+  specialize (He' (<[x := of_val v']> θ) (τ.:δ) (j - 1) W').
+  rewrite <-sem_expr_rel_cons in He'.
+  apply He'.
+  constructor.
+  { eapply val_rel_mono_idx; last done. lia. }
+  apply sem_context_rel_cons.
+  eapply sem_context_rel_mono; last done; [lia | done].
+Qed.
+
+Lemma compat_if n Γ e0 e1 e2 A :
+  TY n; Γ ⊨ e0 : Bool →
+  TY n; Γ ⊨ e1 : A →
+  TY n; Γ ⊨ e2 : A →
+  TY n; Γ ⊨ (if: e0 then e1 else e2) : A.
+Proof.
+  intros He0 He1 He2 θ δ k W Hctx. simpl.
+  specialize (He0 _ _ _ _ Hctx).
+  specialize (He1 _ _ _ _ Hctx).
+  specialize (He2 _ _ _ _ Hctx).
+
+  eapply (bind [IfCtx _ _]); first done.
+  intros j v W' Hj HW Hv.
+  simp type_interp in Hv. destruct Hv as (b & ->).
+  simpl.
+
+  destruct b.
+  - eapply expr_det_step_closure.
+    { apply det_step_if_true. }
+    eapply expr_rel_mono; last done; [lia | done].
+  - eapply expr_det_step_closure.
+    { apply det_step_if_false. }
+    eapply expr_rel_mono; last done; [lia | done].
+Qed.
+
+Lemma compat_pair Δ Γ e1 e2 A B :
+  TY Δ; Γ ⊨ e1 : A →
+  TY Δ; Γ ⊨ e2 : B →
+  TY Δ; Γ ⊨ (e1, e2) : A × B.
+Proof.
+  intros He1 He2 θ δ k W Hctx. simpl.
+  specialize (He1 _ _ _ _ Hctx).
+  specialize (He2 _ _ _ _ Hctx).
+
+  eapply (bind [PairRCtx _]); first done.
+  intros j v2 W' Hj HW Hv2.
+  eapply (bind [PairLCtx _]).
+  { eapply expr_rel_mono; last done; [lia | done]. }
+  intros j' v1 W'' Hj' HW' Hv1.
+
+  simpl.
+  eapply (sem_val_expr_rel _ _ _ _ (v1, v2)%V).
+  simp type_interp. exists v1, v2. split_and!; first done.
+  - done.
+  - eapply val_rel_mono; last done; [lia | done].
+Qed.
+
+Lemma compat_fst Δ Γ e A B :
+  TY Δ; Γ ⊨ e : A × B →
+  TY Δ; Γ ⊨ Fst e : A.
+Proof.
+  intros He θ δ k W Hctx.
+  specialize (He _ _ _ _ Hctx).
+  simpl. eapply (bind [FstCtx]); first done.
+  intros j v W' Hj HW Hv.
+  simp type_interp in Hv. destruct Hv as (v1 & v2 & -> & Hv1 & Hv2).
+
+  eapply expr_det_step_closure.
+  { simpl. apply det_step_fst; apply is_val_of_val. }
+  eapply sem_val_expr_rel. eapply val_rel_mono_idx; last done. lia.
+Qed.
+
+Lemma compat_snd Δ Γ e A B :
+  TY Δ; Γ ⊨ e : A × B →
+  TY Δ; Γ ⊨ Snd e : B.
+Proof.
+  intros He θ δ k w Hctx.
+  specialize (He _ _ _ _ Hctx).
+  simpl. eapply (bind [SndCtx]); first done.
+  intros j v W' Hj HW Hv.
+  simp type_interp in Hv. destruct Hv as (v1 & v2 & -> & Hv1 & Hv2).
+
+  eapply expr_det_step_closure.
+  { simpl. apply det_step_snd; apply is_val_of_val. }
+  eapply sem_val_expr_rel. eapply val_rel_mono_idx; last done. lia.
+Qed.
+
+Lemma compat_injl Δ Γ e A B :
+  TY Δ; Γ ⊨ e : A →
+  TY Δ; Γ ⊨ InjL e : A + B.
+Proof.
+  intros He θ δ k W Hctx. simpl.
+  specialize (He _ _ _ _ Hctx).
+  eapply (bind [InjLCtx]); first done.
+  intros j v W' Hj HW Hv.
+  eapply (sem_val_expr_rel _ _ _ _ (InjLV v)).
+  simp type_interp. left. eauto.
+Qed.
+
+Lemma compat_injr Δ Γ e A B :
+  TY Δ; Γ ⊨ e : B →
+  TY Δ; Γ ⊨ InjR e : A + B.
+Proof.
+  intros He θ δ k W Hctx. simpl.
+  specialize (He _ _ _ _ Hctx).
+  eapply (bind [InjRCtx]); first done.
+  intros j v W' Hj HW Hv.
+  eapply (sem_val_expr_rel _ _ _ _ (InjRV v)).
+  simp type_interp. eauto.
+Qed.
+
+Lemma compat_case Δ Γ e e1 e2 A B C :
+  TY Δ; Γ ⊨ e : B + C →
+  TY Δ; Γ ⊨ e1 : (B → A) →
+  TY Δ; Γ ⊨ e2 : (C → A) →
+  TY Δ; Γ ⊨ Case e e1 e2 : A.
+Proof.
+  intros He He1 He2 θ δ k W Hctx. simpl.
+  specialize (He _ _ _ _ Hctx).
+  specialize (He1 _ _ _ _ Hctx).
+  specialize (He2 _ _ _ _ Hctx).
+  eapply (bind [CaseCtx _ _]); first done.
+  intros j v W' Hj HW Hv.
+  simp type_interp in Hv. destruct Hv as [(v' & -> & Hv') | (v' & -> & Hv')].
+  - simpl. eapply expr_det_step_closure.
+    { apply det_step_casel. apply is_val_of_val. }
+    eapply (bind [AppLCtx _]).
+    { eapply expr_rel_mono; last done; [lia | done]. }
+    intros j' v W'' Hj' HW' Hv. simpl.
+    simp type_interp in Hv. destruct Hv as (x & e' & -> & ? & Hv).
+    eapply expr_det_step_closure. { apply det_step_beta. apply is_val_of_val. }
+    apply Hv; first done. eapply val_rel_mono; last done; [lia | done].
+  - simpl. eapply expr_det_step_closure.
+    { apply det_step_caser. apply is_val_of_val. }
+    eapply (bind [AppLCtx _]).
+    { eapply expr_rel_mono; last done; [lia | done]. }
+    intros j' v W'' Hj' HW' Hv. simpl.
+    simp type_interp in Hv. destruct Hv as (x & e' & -> & ? & Hv).
+    eapply expr_det_step_closure. { apply det_step_beta. apply is_val_of_val. }
+    apply Hv; first done. eapply val_rel_mono; last done; [lia | done].
+Qed.
+
+Lemma compat_roll n Γ e A :
+  TY n; Γ ⊨ e : (A.[(μ: A)%ty/]) →
+  TY n; Γ ⊨ (roll e) : (μ: A).
+Proof.
+  intros He θ δ k W Hctx. simpl.
+  specialize (He _ _ _ _ Hctx).
+
+  eapply (bind [RollCtx]); first done.
+  intros j v W' Hj HW Hv.
+  eapply (sem_val_expr_rel _ _ _ _ (RollV v)).
+
+  specialize (val_rel_is_closed _ _ _ _ _ Hv) as ?.
+  destruct j as [ | j]; simp type_interp; first by eauto.
+  exists v. split_and!; [done.. | ].
+  intros kd. eapply val_rel_mono_idx; last done. lia.
+Qed.
+
+Lemma compat_unroll n Γ e A :
+  TY n; Γ ⊨ e : (μ: A) →
+  TY n; Γ ⊨ (unroll e) : (A.[(μ: A)%ty/]).
+Proof.
+  intros He θ δ k W Hctx. simpl.
+  specialize (He _ _ _ _ Hctx).
+
+  eapply (bind [UnrollCtx]); first done.
+  intros j v W' Hj HW Hv.
+  destruct j as [ | j]; first by apply sem_expr_rel_zero_trivial.
+  simp type_interp in Hv. destruct Hv as (v' & -> & ? & Hv).
+  eapply expr_det_step_closure.
+  { simpl. apply det_step_unroll. apply is_val_of_val. }
+  eapply sem_val_expr_rel. apply Hv.
+Qed.
+
+
+(** A bit of theory about first-order types *)
+Lemma canonical_values_int n Γ e:
+  TY n; Γ ⊢ e : Int →
+  is_val e →
+  ∃ n: Z, e = (#n)%E.
+Proof. inversion 1; simpl; naive_solver. Qed.
+
+Lemma canonical_values_bool n Γ e:
+  TY n; Γ ⊢ e : Bool →
+  is_val e →
+  ∃ b: bool, e = (#b)%E.
+Proof. inversion 1; simpl; naive_solver. Qed.
+
+Lemma canonical_values_unit n Γ e:
+  TY n; Γ ⊢ e : Unit →
+  is_val e →
+  e = (#LitUnit)%E.
+Proof. inversion 1; simpl; naive_solver. Qed.
+
+Lemma canonical_values_prod n Γ e A B :
+  TY n; Γ ⊢ e : A × B →
+  is_val e →
+  ∃ e1 e2, e = (e1, e2)%E ∧ is_val e1 ∧ is_val e2 ∧
+    TY n; Γ ⊢ e1 : A ∧ TY n; Γ ⊢ e2 : B .
+Proof. inversion 1; simpl; naive_solver. Qed.
+
+Lemma canonical_values_sum n Γ e A B :
+  TY n; Γ ⊢ e : A + B →
+  is_val e →
+  (∃ e', e = InjL e' ∧ is_val e' ∧ TY n; Γ ⊢ e' : A) ∨ (∃ e', e = InjR e' ∧ is_val e' ∧ TY n; Γ ⊢ e' : B).
+Proof. inversion 1; simpl; naive_solver. Qed.
+
+Lemma type_wf_fotype a : type_wf 0 a.
+Proof. induction a; simpl; eauto. Qed.
+
+(* First-order types are simple. *)
+Lemma syn_fo_typed_val a δ k W v :
+  TY 0; ∅ ⊢ of_val v : a ↔ 𝒱 a δ k W v.
+Proof.
+  induction a as [ | | | a1 IH1 a2 IH2 | a1 IH1 a2 IH2 ] in v |-*.
+  - split.
+    + intros [z Heq]%canonical_values_int; simplify_val; last eauto.
+      simp type_interp. eauto.
+    + simp type_interp. intros (z & ->). constructor.
+  - split.
+    + intros (b & Heq)%canonical_values_bool; simplify_val; last eauto.
+      simp type_interp. eauto.
+    + simp type_interp. intros (b & ->). constructor.
+  - split.
+    + intros Heq%canonical_values_unit; simplify_val; last eauto.
+      simp type_interp; eauto.
+    + simp type_interp. intros ->. econstructor.
+  - split.
+    + simpl. intros (e1 & e2 & ? & (v1 & Heq1)%is_val_spec & (v2 & Heq2)%is_val_spec & H1 & H2)%canonical_values_prod; last eauto.
+      simplify_val. apply of_val_pair_inv in H; subst v.
+      simp type_interp. exists v1, v2. naive_solver.
+    + simpl. simp type_interp. intros (v1 & v2 & -> & Hv1%IH1 & Hv2%IH2). econstructor; done.
+  - split.
+    + simpl. intros [(e & ? & (v' & Heq)%is_val_spec & H) | (e & ? & (v' & Heq)%is_val_spec & H)]%canonical_values_sum; last eauto.
+      * simplify_val. apply of_val_injl_inv in H0; subst v.
+        simp type_interp. left. naive_solver.
+      * simplify_val. apply of_val_injr_inv in H0; subst v.
+        simp type_interp. right. naive_solver.
+    + simpl. simp type_interp. intros [(v' & -> & Hv%IH1) | (v' & -> & Hv%IH2)].
+      * simpl. eapply typed_injl; last done. apply type_wf_fotype.
+      * simpl. eapply typed_injr; last done. apply type_wf_fotype.
+Qed.
+
+Lemma wsat_init_heap σ l v a W :
+  σ !! l = None →
+  wsat W σ →
+  TY 0; ∅ ⊢ v : a →
+  wsat ((λ σ, ∃ v, σ = <[l := v]> ∅ ∧ TY 0; ∅ ⊢ v : a) :: W) (init_heap l 1 v σ).
+Proof.
+  intros. simpl. eexists. split; [exists v; split; [reflexivity | ] | split ].
+  - done.
+  - unfold init_heap. simpl. rewrite right_id.
+    rewrite -insert_union_singleton_l. apply insert_mono.
+    apply map_empty_subseteq.
+  - unfold init_heap. simpl. rewrite right_id. rewrite -delete_difference map_difference_empty.
+    rewrite delete_union delete_singleton left_id.
+    rewrite delete_notin; done.
+Qed.
+
+Lemma compat_new Δ Γ e a :
+  TY Δ; Γ ⊨ e : a →
+  TY Δ; Γ ⊨ new e : (Ref a).
+Proof.
+  intros He θ δ k W Hctx.
+  eapply (bind [NewCtx]). { eapply He; done. }
+  intros j v W' Hj Hext Hv.
+  simp type_interp.
+
+  intros e' σ σ' W'' n Hext' Hsat' Hn Hred.
+  eapply new_nsteps_inv in Hred as [-> Hstep]; last apply to_of_val.
+  eapply new_step_inv in Hstep as (l & -> & -> & ?); last apply to_of_val.
+  exists #l, ((λ σ', ∃ v, σ' = <[ l := v ]> ∅ ∧ TY 0; ∅ ⊢ (of_val v) : a) :: W'').
+  split_and!; [done | eapply suffix_cons_l; reflexivity | .. ].
+  { apply wsat_init_heap; [ done.. | ].
+    by eapply syn_fo_typed_val.
+  }
+  simp type_interp.
+  exists l. split; first done. eexists 0, _. split; done.
+Qed.
+
+Lemma compat_load Δ Γ e a :
+  TY Δ; Γ ⊨ e : Ref a →
+  TY Δ; Γ ⊨ !e : a.
+Proof.
+  intros He θ δ k W Hctx.
+  eapply (bind [LoadCtx]). { eapply He; done. }
+  intros j v W' Hj Hext Hv.
+  simp type_interp in Hv.
+  destruct Hv as (l & -> & (i & INV & Hlook & ->)).
+
+  simp type_interp.
+
+  intros e' σ σ' W'' n Hext' Hsat' Hn.
+  eapply wsat_lookup in Hlook; last by eapply wsat_wext.
+  destruct Hlook as (? & Hincl & (v & -> & ?)).
+  intros Hred. eapply load_nsteps_inv in Hred as [(-> & -> & -> & Hirred) | [-> Hstep]]; last apply to_of_val.
+  { exfalso; apply Hirred.
+    exists (of_val v), σ. apply base_contextual_step.
+    econstructor. eapply lookup_weaken; last done. apply lookup_insert.
+  }
+  eapply load_step_inv in Hstep; last apply to_of_val.
+  destruct Hstep as (? & v' & [= <-] & Hl & -> & ->).
+  eapply lookup_weaken_inv in Hincl; [ | apply lookup_insert | done]. subst v'.
+  rewrite to_of_val. eexists _, _. split_and!; [reflexivity | reflexivity | done | ].
+
+  (* use that FO types are simple. *)
+  apply syn_fo_typed_val; done.
+Qed.
+
+Lemma compat_store Δ Γ e1 e2 a :
+  TY Δ; Γ ⊨ e1 : Ref a →
+  TY Δ; Γ ⊨ e2 : a →
+  TY Δ; Γ ⊨ (e1 <- e2) : Unit.
+Proof.
+  (* you may find the lemmas [wsat_lookup, wsat_update] above helpful. *)
+  intros He1 He2 θ δ k W Hctx. simpl.
+  eapply (bind [StoreRCtx _]). { eapply He2; done. }
+  intros j v W' Hj Hext Hv2.
+
+  eapply (bind [StoreLCtx _]).
+  { eapply expr_rel_mono; last eapply He1; done. }
+  intros j' v' W'' Hj' Hext' Hv1.
+  simp type_interp in Hv1.
+  destruct Hv1 as (l & -> & (i & INV & Hlook & ->)).
+
+  simp type_interp.
+  intros e' σ σ' W''' n Hext'' Hsat' Hn.
+  specialize (wsat_lookup W'' _ i _ ltac:(by eapply wsat_wext) Hlook) as (? & Hincl & (vm & -> & ?)).
+
+  intros [(-> & -> & -> & Hirred) | [-> Hstep]]%store_nsteps_inv.
+  { exfalso; apply Hirred.
+    exists (Lit LitUnit), (<[l := v]> σ). apply base_contextual_step.
+    econstructor. 2: by rewrite to_of_val.
+    eapply lookup_weaken; last done. apply lookup_insert.
+  }
+  apply store_step_inv in Hstep.
+  destruct Hstep as (? & v' & [= <-] & Hl & -> & ->).
+  eexists _, _. split_and!; [reflexivity | reflexivity | | ].
+  2: { simp type_interp. done. }
+
+  (* restore the invariant *)
+  destruct Hext'' as (Pre & ->).
+  eapply (wsat_update _ _ (length Pre + i) _ _ ); [ done | ..].
+  { rewrite lookup_app_r; last lia.
+    replace (length Pre + i - length Pre) with i by lia.
+    done.
+  }
+  intros σ' (v'' & -> & _). split.
+  { apply lookup_insert_is_Some. by left. }
+  exists v. rewrite insert_insert. split; first done.
+  eapply syn_fo_typed_val; done.
+Qed.
+
+
+Local Hint Resolve compat_var compat_lam_named compat_lam_anon compat_tlam compat_int compat_bool compat_unit compat_if compat_app compat_tapp compat_pack compat_unpack compat_int_binop compat_int_bool_binop compat_unop compat_pair compat_fst compat_snd compat_injl compat_injr compat_case compat_roll compat_unroll compat_new compat_store compat_load: core.
+
+Lemma sem_soundness Δ Γ e A :
+  TY Δ; Γ ⊢ e : A →
+  TY Δ; Γ ⊨ e : A.
+Proof.
+  induction 1 as [ | Δ Γ x e A B Hsyn IH | Δ Γ e A B Hsyn IH| Δ Γ e A Hsyn IH| | | | |  | | | | n Γ e1 e2 op A B C Hop ? ? ? ? | | | | | | | | |  | | | ]; eauto.
+  - (* lambda *)
+    set (X := elements (dom (<[x := A]>Γ))).
+    specialize (syn_typed_closed _ _ _ _ X Hsyn) as Hcl.
+    eapply compat_lam_named; last done.
+    + apply Hcl. apply elem_of_elements.
+    + intros ??. by apply elem_of_elements.
+  - (* lambda anon *)
+    set (X := elements (dom Γ)).
+    specialize (syn_typed_closed _ _ _ _ X Hsyn) as Hcl.
+    eapply compat_lam_anon; last done.
+    + apply Hcl. apply elem_of_elements.
+    + intros ??. by apply elem_of_elements.
+  - (* tlam *)
+    set (X := elements (dom Γ)).
+    specialize (syn_typed_closed _ _ _ _ X Hsyn) as Hcl.
+    eapply compat_tlam; last done.
+    + apply Hcl. rewrite dom_fmap. apply elem_of_elements.
+    + intros ??. by apply elem_of_elements.
+  - (* binop *) inversion Hop; subst; eauto.
+Qed.
+
+(* dummy delta which we can use if we don't care *)
+Program Definition any_type : sem_type := {| sem_type_car := λ k W v, is_closed [] v |}.
+Definition δ_any : var → sem_type := λ _, any_type.
+
+
+Definition safe e h :=
+  ∀ e' h' n, red_nsteps n e h e' h' → is_val e'.
+
+Lemma type_safety e A :
+  TY 0; ∅ ⊢ e : A →
+  safe e ∅.
+Proof.
+  intros He%sem_soundness e' h' n Hred.
+  specialize (He ∅ δ_any (S n) []). simp type_interp in He.
+  rewrite subst_map_empty in He.
+  edestruct (He ) as (v & W' & Hv & _); [ | done | | | eassumption | ].
+  - constructor.
+  - done.
+  - lia.
+  - rewrite <- (of_to_val _ _ Hv). apply is_val_of_val.
+Qed.
+
+
+(** Additional lemmas *)
+Lemma semantic_app A B δ k W e1 e2 :
+  ℰ (A → B) δ k W e1 →
+  ℰ A δ k W e2 →
+  ℰ B δ k W (e1 e2).
+Proof.
+  intros He1 He2.
+  eapply (bind [AppRCtx e1]); first done.
+  intros j v W' Hj Hincl Hv. eapply (bind [AppLCtx _]).
+  { eapply expr_rel_mono; [ | done..]. lia. }
+  intros j' v' W'' Hj' Hincl' Hf.
+  simp type_interp in Hf. destruct Hf as (x & e & -> & Hcl & Hf).
+  eapply expr_det_step_closure.
+  { apply det_step_beta. apply is_val_of_val. }
+  apply Hf; first done.
+  eapply val_rel_mono; [ | done..]. lia.
+Qed.
diff --git a/theories/type_systems/systemf_mu_state/types_sol.v b/theories/type_systems/systemf_mu_state/types_sol.v
new file mode 100644
index 0000000..79f3741
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/types_sol.v
@@ -0,0 +1,1337 @@
+From stdpp Require Import base relations.
+From iris Require Import prelude.
+From semantics.lib Require Import maps.
+From semantics.ts.systemf_mu_state Require Import lang notation.
+From Autosubst Require Export Autosubst.
+
+(** ** Syntactic typing *)
+(** We use De Bruijn indices with the help of the Autosubst library. *)
+Inductive type : Type :=
+  (** [var] is the type of variables of Autosubst -- it unfolds to [nat] *)
+  | TVar : var → type
+  | Int
+  | Bool
+  | Unit
+  (** The [{bind 1 of type}] tells Autosubst to put a De Bruijn binder here *)
+  | TForall : {bind 1 of type} → type
+  | TExists : {bind 1 of type} → type
+  | Fun (A B : type)
+  | Prod (A B : type)
+  | Sum (A B : type)
+  | TMu : {bind 1 of type} → type
+  | Ref (A : type)
+.
+
+(** Autosubst instances.
+  This lets Autosubst do its magic and derive all the substitution functions, etc.
+ *)
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+
+Definition typing_context := gmap string type.
+Definition heap_context := gmap loc type.
+Implicit Types
+  (Γ : typing_context)
+  (Σ : heap_context)
+  (v : val)
+  (e : expr)
+  (A B : type)
+.
+
+Declare Scope FType_scope.
+Delimit Scope FType_scope with ty.
+Bind Scope FType_scope with type.
+Notation "# x" := (TVar x) : FType_scope.
+Infix "→" := Fun : FType_scope.
+Notation "(→)" := Fun (only parsing) : FType_scope.
+Notation "∀: τ" :=
+  (TForall τ%ty)
+  (at level 100, τ at level 200) : FType_scope.
+Notation "∃: τ" :=
+  (TExists τ%ty)
+  (at level 100, τ at level 200) : FType_scope.
+Infix "×" := Prod (at level 70) : FType_scope.
+Notation "(×)" := Prod (only parsing) : FType_scope.
+Infix "+" := Sum : FType_scope.
+Notation "(+)" := Sum (only parsing) : FType_scope.
+Notation "μ: A" :=
+  (TMu A%ty)
+  (at level 100, A at level 200) : FType_scope.
+
+(** Shift all the indices in the context by one,
+   used when inserting a new type interpretation in Δ. *)
+(* [<$>] is notation for the [fmap] operation that maps the substitution over the whole map. *)
+(* [ren] is Autosubst's renaming operation -- it renames all type variables according to the given function,
+  in this case [(+1)] to shift the variables up by 1. *)
+Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)) <$> Γ) (at level 10, format "⤉ Γ").
+
+
+(** [type_wf n A] states that a type [A] has only free variables up to < [n].
+ (in other words, all variables occurring free are strictly bounded by [n]). *)
+Inductive type_wf : nat → type → Prop :=
+  | type_wf_TVar m n:
+      m < n →
+      type_wf n (TVar m)
+  | type_wf_Int n: type_wf n Int
+  | type_wf_Bool n : type_wf n Bool
+  | type_wf_Unit n : type_wf n Unit
+  | type_wf_TForall n A :
+      type_wf (S n) A →
+      type_wf n (TForall A)
+  | type_wf_TExists n A :
+      type_wf (S n) A →
+      type_wf n (TExists A)
+  | type_wf_Fun n A B:
+      type_wf n A →
+      type_wf n B →
+      type_wf n (Fun A B)
+  | type_wf_Prod n A B :
+      type_wf n A →
+      type_wf n B →
+      type_wf n (Prod A B)
+  | type_wf_Sum n A B :
+      type_wf n A →
+      type_wf n B →
+      type_wf n (Sum A B)
+  | type_wf_mu n A :
+      type_wf (S n) A →
+      type_wf n (μ: A)
+  | type_wf_ref n A :
+      type_wf n A →
+      type_wf n (Ref A)
+.
+#[export] Hint Constructors type_wf : core.
+
+Inductive bin_op_typed : bin_op → type → type → type → Prop :=
+  | plus_op_typed : bin_op_typed PlusOp Int Int Int
+  | minus_op_typed : bin_op_typed MinusOp Int Int Int
+  | mul_op_typed : bin_op_typed MultOp Int Int Int
+  | lt_op_typed : bin_op_typed LtOp Int Int Bool
+  | le_op_typed : bin_op_typed LeOp Int Int Bool
+  | eq_op_typed : bin_op_typed EqOp Int Int Bool.
+#[export] Hint Constructors bin_op_typed : core.
+
+Inductive un_op_typed : un_op → type → type → Prop :=
+  | neg_op_typed : un_op_typed NegOp Bool Bool
+  | minus_un_op_typed : un_op_typed MinusUnOp Int Int.
+
+Reserved Notation "'TY' Σ ; n ; Γ ⊢ e : A" (at level 74, e, A at next level).
+Inductive syn_typed : heap_context → nat → typing_context → expr → type → Prop :=
+  | typed_var Σ n Γ x A :
+      Γ !! x = Some A →
+      TY Σ; n; Γ ⊢ (Var x) : A
+  | typed_lam Σ n Γ x e A B :
+      TY Σ; n ; (<[ x := A]> Γ) ⊢ e : B →
+      type_wf n A →
+      TY Σ; n; Γ ⊢ (Lam (BNamed x) e) : (A → B)
+  | typed_lam_anon Σ n Γ e A B :
+      TY Σ; n ; Γ ⊢ e : B →
+      type_wf n A →
+      TY Σ; n; Γ ⊢ (Lam BAnon e) : (A → B)
+  | typed_tlam Σ n Γ e A :
+      (* we need to shift the context up as we descend under a binder *)
+      TY (⤉ Σ); S n; (⤉ Γ) ⊢ e : A →
+      TY Σ; n; Γ ⊢ (Λ, e) : (∀: A)
+  | typed_tapp Σ n Γ A B e :
+      TY Σ; n; Γ ⊢ e : (∀: A) →
+      type_wf n B →
+      (* A.[B/] is the notation for Autosubst's substitution operation that
+        replaces variable 0 by [B] *)
+      TY Σ; n; Γ ⊢ (e <>) : (A.[B/])
+  | typed_pack Σ n Γ A B e :
+      type_wf n B →
+      type_wf (S n) A →
+      TY Σ; n; Γ ⊢ e : (A.[B/]) →
+      TY Σ; n; Γ ⊢ (pack e) : (∃: A)
+  | typed_unpack Σ n Γ A B e e' x :
+      type_wf n B → (* we should not leak the existential! *)
+      TY Σ; n; Γ ⊢ e : (∃: A) →
+      (* As we descend under a type variable binder for the typing of [e'],
+          we need to shift the indices in [Γ] and [B] up by one.
+        On the other hand, [A] is already defined under this binder, so we need not shift it.
+      *)
+      TY (⤉ Σ); (S n); (<[x := A]>(⤉Γ)) ⊢ e' : (B.[ren (+1)]) →
+      TY Σ; n; Γ ⊢ (unpack e as BNamed x in e') : B
+  | typed_int Σ n Γ z : TY Σ; n; Γ ⊢ (Lit $ LitInt z) : Int
+  | typed_bool Σ n Γ b : TY Σ; n; Γ ⊢ (Lit $ LitBool b) : Bool
+  | typed_unit Σ n Γ : TY Σ; n; Γ ⊢ (Lit $ LitUnit) : Unit
+  | typed_if Σ n Γ e0 e1 e2 A :
+      TY Σ; n; Γ ⊢ e0 : Bool →
+      TY Σ; n; Γ ⊢ e1 : A →
+      TY Σ; n; Γ ⊢ e2 : A →
+      TY Σ; n; Γ ⊢ If e0 e1 e2 : A
+  | typed_app Σ n Γ e1 e2 A B :
+      TY Σ; n; Γ ⊢ e1 : (A → B) →
+      TY Σ; n; Γ ⊢ e2 : A →
+      TY Σ; n; Γ ⊢ (e1 e2)%E : B
+  | typed_binop Σ n Γ e1 e2 op A B C :
+      bin_op_typed op A B C →
+      TY Σ; n; Γ ⊢ e1 : A →
+      TY Σ; n; Γ ⊢ e2 : B →
+      TY Σ; n; Γ ⊢ BinOp op e1 e2 : C
+  | typed_unop Σ n Γ e op A B :
+      un_op_typed op A B →
+      TY Σ; n; Γ ⊢ e : A →
+      TY Σ; n; Γ ⊢ UnOp op e : B
+  | typed_pair Σ n Γ e1 e2 A B :
+      TY Σ; n; Γ ⊢ e1 : A →
+      TY Σ; n; Γ ⊢ e2 : B →
+      TY Σ; n; Γ ⊢ (e1, e2) : A × B
+  | typed_fst Σ n Γ e A B :
+      TY Σ; n; Γ ⊢ e : A × B →
+      TY Σ; n; Γ ⊢ Fst e : A
+  | typed_snd Σ n Γ e A B :
+      TY Σ; n; Γ ⊢ e : A × B →
+      TY Σ; n; Γ ⊢ Snd e : B
+  | typed_injl Σ n Γ e A B :
+      type_wf n B →
+      TY Σ; n; Γ ⊢ e : A →
+      TY Σ; n; Γ ⊢ InjL e : A + B
+  | typed_injr Σ n Γ e A B :
+      type_wf n A →
+      TY Σ; n; Γ ⊢ e : B →
+      TY Σ; n; Γ ⊢ InjR e : A + B
+  | typed_case Σ n Γ e e1 e2 A B C :
+      TY Σ; n; Γ ⊢ e : B + C →
+      TY Σ; n; Γ ⊢ e1 : (B → A) →
+      TY Σ; n; Γ ⊢ e2 : (C → A) →
+      TY Σ; n; Γ ⊢ Case e e1 e2 : A
+  | typed_roll Σ n Γ e A :
+      TY Σ; n; Γ ⊢ e : (A.[(μ: A)/]) →
+      TY Σ; n; Γ ⊢ (roll e) : (μ: A)
+  | typed_unroll Σ n Γ e A :
+      TY Σ; n; Γ ⊢ e : (μ: A) →
+      TY Σ; n; Γ ⊢ (unroll e) : (A.[(μ: A)/])
+  | typed_loc Σ Δ Γ l A :
+      Σ !! l = Some A →
+      TY Σ; Δ; Γ ⊢ (Lit $ LitLoc l) : (Ref A)
+  | typed_load Σ Δ Γ e A :
+      TY Σ; Δ; Γ ⊢ e : (Ref A) →
+      TY Σ; Δ; Γ ⊢ !e : A
+  | typed_store Σ Δ Γ e1 e2 A :
+      TY Σ; Δ; Γ ⊢ e1 : (Ref A) →
+      TY Σ; Δ; Γ ⊢ e2 : A →
+      TY Σ; Δ; Γ ⊢ (e1 <- e2) : Unit
+  | typed_new Σ Δ Γ e A :
+      TY Σ; Δ; Γ ⊢ e : A →
+      TY Σ; Δ; Γ ⊢ (new e) : Ref A
+where "'TY' Σ ; n ; Γ ⊢ e : A" := (syn_typed Σ n Γ e%E A%ty).
+#[export] Hint Constructors syn_typed : core.
+
+(** Examples *)
+Goal TY ∅; 0; ∅ ⊢ (λ: "x", #1 + "x")%E : (Int → Int).
+Proof. eauto. Qed.
+(** [∀: #0 → #0] corresponds to [∀ α. α → α] with named binders. *)
+Goal TY ∅; 0; ∅ ⊢ (Λ, λ: "x", "x")%E : (∀: #0 → #0).
+Proof. repeat econstructor. Qed.
+Goal TY ∅; 0; ∅ ⊢ (pack ((λ: "x", "x"), #42)) : ∃: (#0 → #0) × #0.
+Proof.
+  apply (typed_pack _ _ _ _ Int).
+  - eauto.
+  - repeat econstructor.
+  - (* [asimpl] is Autosubst's tactic for simplifying goals involving type substitutions. *)
+    asimpl. eauto.
+Qed.
+Goal TY ∅; 0; ∅ ⊢ (unpack (pack ((λ: "x", "x"), #42)) as "y" in (λ: "x", #1337) ((Fst "y") (Snd "y"))) : Int.
+Proof.
+  (* if we want to typecheck stuff with existentials, we need a bit more explicit proofs.
+    Letting eauto try to instantiate the evars becomes too expensive. *)
+  apply (typed_unpack _ _ _ ((#0 → #0) × #0)%ty).
+  - done.
+  - apply (typed_pack _ _ _ _ Int); asimpl; eauto.
+    repeat econstructor.
+  - eapply (typed_app _ _ _ _ _ (#0)%ty); eauto 10.
+Qed.
+
+(** fails: we are not allowed to leak the existential *)
+Goal TY ∅; 0; ∅ ⊢ (unpack (pack ((λ: "x", "x"), #42)) as "y" in (Fst "y") (Snd "y")) : #0.
+Proof.
+  apply (typed_unpack _ _ _ ((#0 → #0) × #0)%ty).
+Abort.
+
+(* derived typing rule for match *)
+Lemma typed_match Σ n Γ e e1 e2 x1 x2 A B C :
+  type_wf n B →
+  type_wf n C →
+  TY Σ; n; Γ ⊢ e : B + C →
+  TY Σ; n; <[x1 := B]> Γ ⊢ e1 : A →
+  TY Σ; n; <[x2 := C]> Γ ⊢ e2 : A →
+  TY Σ; n; Γ ⊢ match: e with InjL (BNamed x1) => e1 | InjR (BNamed x2) => e2 end : A.
+Proof. eauto. Qed.
+
+Lemma syn_typed_closed Σ n Γ e A X :
+  TY Σ; n; Γ ⊢ e : A →
+  (∀ x, x ∈ dom Γ → x ∈ X) →
+  is_closed X e.
+Proof.
+  induction 1 as [ | ???????? IH | | Σ n Γ e A H IH | | | Σ n Γ A B e e' x Hwf H1 IH1 H2 IH2 | | | | | | | | | | | | | | | | | | | ] in X |-*; simpl; intros Hx; try done.
+
+  { (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. }
+  { (* lam *) apply IH.
+    intros y. rewrite elem_of_dom lookup_insert_is_Some.
+    intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
+    apply elem_of_cons. right. eapply Hx. by apply elem_of_dom.
+  }
+  { (* anon lam *) naive_solver. }
+  { (* tlam *)
+    eapply IH. intros x Hel. apply Hx.
+    by rewrite dom_fmap in Hel.
+  }
+  3: { (* unpack *)
+    apply andb_True; split.
+    - apply IH1. apply Hx.
+    - apply IH2. intros y. rewrite elem_of_dom lookup_insert_is_Some.
+    intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
+    apply elem_of_cons. right. eapply Hx.
+    apply elem_of_dom. revert Hy. rewrite lookup_fmap fmap_is_Some. done.
+  }
+  (* everything else *)
+  all: repeat match goal with
+              | |- Is_true (_ && _)  => apply andb_True; split
+              end.
+  all: try naive_solver.
+Qed.
+
+(** *** Lemmas about [type_wf] *)
+Lemma type_wf_mono n m A:
+  type_wf n A → n ≤ m → type_wf m A.
+Proof.
+  induction 1 in m |-*; eauto with lia.
+Qed.
+
+Lemma type_wf_rename n A δ:
+  type_wf n A →
+  (∀ i j, i < j → δ i < δ j) →
+  type_wf (δ n) (rename δ A).
+Proof.
+  induction 1 in δ |-*; intros Hmon; simpl; eauto.
+  all: econstructor; eapply type_wf_mono; first eapply IHtype_wf; last done.
+  all: intros i j Hlt; destruct i, j; simpl; try lia.
+  all: rewrite -Nat.succ_lt_mono; eapply Hmon; lia.
+Qed.
+
+(** [A.[σ]], i.e. [A] with the substitution [σ] applied to it, is well-formed under [m] if
+   [A] is well-formed under [n] and all the things we substitute up to [n] are well-formed under [m].
+ *)
+Lemma type_wf_subst n m A σ:
+  type_wf n A →
+  (∀ x, x < n → type_wf m (σ x)) →
+  type_wf m A.[σ].
+Proof.
+  induction 1 in m, σ |-*; intros Hsub; simpl; eauto.
+  + econstructor; eapply IHtype_wf.
+    intros [|x]; rewrite /up //=.
+    - econstructor. lia.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
+      intros i j Hlt'; simpl; lia.
+  + econstructor; eapply IHtype_wf.
+    intros [|x]; rewrite /up //=.
+    - econstructor. lia.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
+      intros i j Hlt'; simpl; lia.
+  + econstructor. eapply IHtype_wf.
+    intros [|x]; rewrite /up //=.
+    - econstructor. lia.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
+      intros ???. simpl; lia.
+Qed.
+
+Fixpoint free_vars A : nat → Prop :=
+  match A with
+  | TVar n => λ m, m = n
+  | Int => λ _, False
+  | Bool => λ _, False
+  | Unit => λ _, False
+  | Fun A B => λ n, free_vars A n ∨ free_vars B n
+  | Prod A B => λ n, free_vars A n ∨ free_vars B n
+  | Sum A B => λ n, free_vars A n ∨ free_vars B n
+  | TForall A => λ n, free_vars A (S n)
+  | TExists A => λ n, free_vars A (S n)
+  | TMu A => λ n, free_vars A (S n)
+  | Ref A => λ n, free_vars A n
+  end.
+
+Definition bounded n A :=
+  (∀ x, free_vars A x → x < n).
+
+Lemma type_wf_bounded n A:
+  type_wf n A ↔ bounded n A.
+Proof.
+  rewrite /bounded; split.
+  - induction 1; simpl; try naive_solver.
+    + intros x Hfree % IHtype_wf. lia.
+    + intros x Hfree % IHtype_wf. lia.
+    + intros x Hfree % IHtype_wf. lia.
+  - induction A in n |-*; simpl; eauto.
+    + intros Hsub. econstructor. eapply IHA.
+      intros ??. destruct x as [|x]; first lia.
+      eapply Hsub in H. lia.
+    + intros Hsub. econstructor. eapply IHA.
+      intros ??. destruct x as [|x]; first lia.
+      eapply Hsub in H. lia.
+    + intros Hsub. econstructor; eauto.
+    + intros Hsub. econstructor; eauto.
+    + intros Hsub. econstructor; eauto.
+    + intros Hsub. econstructor. eapply IHA.
+      intros ??. destruct x as [|x]; first lia.
+      eapply Hsub in H. lia.
+Qed.
+
+Lemma free_vars_rename A x δ:
+  free_vars A x → free_vars (rename δ A) (δ x).
+Proof.
+  induction A in x, δ |-*; simpl; try naive_solver.
+  - intros Hf. apply (IHA (S x) (upren δ) Hf).
+  - intros Hf. apply (IHA (S x) (upren δ) Hf).
+  - intros Hf. apply (IHA (S x) (upren δ) Hf).
+Qed.
+
+Lemma free_vars_subst x n A σ :
+  bounded n A.[σ] → free_vars A x → bounded n (σ x).
+Proof.
+  induction A in n, σ, x |-*; simpl; try naive_solver.
+  - rewrite -type_wf_bounded. inversion 1; subst. revert H2; clear H.
+    rewrite type_wf_bounded.
+    intros Hbd Hfree. eapply IHA in Hbd; last done.
+    revert Hbd. rewrite /up //=.
+    intros Hbd y Hf. enough (S y < S n) by lia.
+    eapply Hbd. simpl. by eapply free_vars_rename.
+  - rewrite -type_wf_bounded. inversion 1; subst. revert H2; clear H.
+    rewrite type_wf_bounded.
+    intros Hbd Hfree. eapply IHA in Hbd; last done.
+    revert Hbd. rewrite /up //=.
+    intros Hbd y Hf. enough (S y < S n) by lia.
+    eapply Hbd. simpl. by eapply free_vars_rename.
+  - rewrite -!type_wf_bounded. inversion 1; subst.
+    revert H3 H4. rewrite !type_wf_bounded. naive_solver.
+  - rewrite -!type_wf_bounded. inversion 1; subst.
+    revert H3 H4. rewrite !type_wf_bounded. naive_solver.
+  - rewrite -!type_wf_bounded. inversion 1; subst.
+    revert H3 H4. rewrite !type_wf_bounded. naive_solver.
+  - rewrite -type_wf_bounded. inversion 1; subst. revert H2; clear H.
+    rewrite type_wf_bounded.
+    intros Hbd Hfree. eapply IHA in Hbd; last done.
+    revert Hbd. rewrite /up //=.
+    intros Hbd y Hf. enough (S y < S n) by lia.
+    eapply Hbd. simpl. by eapply free_vars_rename.
+Qed.
+
+Lemma type_wf_rec_type n A:
+  type_wf n A.[(μ: A)%ty/] → type_wf (S n) A.
+Proof.
+  rewrite !type_wf_bounded. intros Hbound x Hfree.
+  eapply free_vars_subst in Hbound; last done.
+  destruct x as [|x]; first lia; simpl in Hbound.
+  eapply type_wf_bounded in Hbound. inversion Hbound; subst; lia.
+Qed.
+
+Lemma type_wf_single_subst n A B: type_wf n B → type_wf (S n) A → type_wf n A.[B/].
+Proof.
+  intros HB HA. eapply type_wf_subst; first done.
+  intros [|x]; simpl; eauto.
+  intros ?; econstructor. lia.
+Qed.
+
+(** We lift [type_wf] to well-formedness of contexts *)
+Definition ctx_wf n Γ := (∀ x A, Γ !! x = Some A → type_wf n A).
+
+Lemma ctx_wf_empty n : ctx_wf n ∅.
+Proof. rewrite /ctx_wf. set_solver. Qed.
+
+Lemma ctx_wf_insert n x Γ A: ctx_wf n Γ → type_wf n A → ctx_wf n (<[x := A]> Γ).
+Proof. intros H1 H2 y B. rewrite lookup_insert_Some. naive_solver. Qed.
+
+Lemma ctx_wf_up n Γ:
+  ctx_wf n Γ → ctx_wf (S n) (⤉Γ).
+Proof.
+  intros Hwf x A; rewrite lookup_fmap.
+  intros (B & Hlook & ->) % fmap_Some.
+  asimpl. eapply type_wf_subst; first eauto.
+  intros y Hlt. simpl. econstructor. lia.
+Qed.
+
+Definition heap_ctx_wf Δ (Σ: heap_context) := (∀ x A, Σ !! x = Some A → type_wf Δ A).
+
+Lemma heap_ctx_wf_empty n : heap_ctx_wf n ∅.
+Proof. rewrite /heap_ctx_wf. set_solver. Qed.
+
+Lemma heap_ctx_wf_insert n l Σ A: heap_ctx_wf n Σ → type_wf n A → heap_ctx_wf n (<[l := A]> Σ).
+Proof. intros H1 H2 y B. rewrite lookup_insert_Some. naive_solver. Qed.
+
+Lemma heap_ctx_wf_up n Σ:
+  heap_ctx_wf n Σ → heap_ctx_wf (S n) (⤉Σ).
+Proof.
+  intros Hwf x A; rewrite lookup_fmap.
+  intros (B & Hlook & ->) % fmap_Some.
+  asimpl. eapply type_wf_subst; first eauto.
+  intros y Hlt. simpl. econstructor. lia.
+Qed.
+
+#[global]
+Hint Resolve ctx_wf_empty ctx_wf_insert ctx_wf_up heap_ctx_wf_up heap_ctx_wf_empty heap_ctx_wf_empty : core.
+
+(** Well-typed terms at [A] under a well-formed context have well-formed types [A].*)
+Lemma syn_typed_wf Σ n Γ e A:
+  ctx_wf n Γ →
+  heap_ctx_wf n Σ →
+  TY Σ; n; Γ ⊢ e : A →
+  type_wf n A.
+Proof.
+  intros Hwf Hhwf; induction 1 as [ | Σ n Γ x e A B Hty IH Hwfty | | Σ n Γ e A Hty IH | Σ n Γ A B e Hty IH Hwfty | Σ n Γ A B e Hwfty Hty IH| | |  | | | Σ n Γ e1 e2 A B HtyA IHA HtyB IHB | Σ n Γ e1 e2 op A B C Hop HtyA IHA HtyB IHB | Σ n Γ e op A B Hop H IH | Σ n Γ e1 e2 A B HtyA IHA HtyB IHB | Σ n Γ e A B Hty IH | Σ n Γ e A B Hty IH | Σ n Γ e A B Hwfty Hty IH | Σ n Γ e A B Hwfty Hty IH| Σ n Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2 | Σ n Γ e A Hty IH | Σ n Γ e A Hty IH | Σ n Γ l A Hlook| Σ n Γ e A Hty IH | Σ n Γ e1 e2 A Hty1 IH1 Hty2 IH2 | Σ n Γ e A Hty IH]; eauto.
+  - eapply type_wf_single_subst; first done.
+    specialize (IH Hwf Hhwf) as Hwf'.
+    by inversion Hwf'.
+  - specialize (IHA Hwf Hhwf) as Hwf'.
+    by inversion Hwf'; subst.
+  - inversion Hop; subst; eauto.
+  - inversion Hop; subst; eauto.
+  - specialize (IH Hwf Hhwf) as Hwf'. by inversion Hwf'; subst.
+  - specialize (IH Hwf Hhwf) as Hwf'. by inversion Hwf'; subst.
+  - specialize (IHe1 Hwf Hhwf) as Hwf''. by inversion Hwf''; subst.
+  - specialize (IH Hwf Hhwf) as Hwf'%type_wf_rec_type.
+    by econstructor.
+  - eapply type_wf_single_subst; first by apply IH.
+    specialize (IH Hwf Hhwf) as Hwf'.
+    by inversion Hwf'.
+  - specialize (IH Hwf Hhwf) as Hwf'. by inversion Hwf'.
+Qed.
+
+Lemma renaming_ctx_inclusion Γ Δ : Γ ⊆ Δ → ⤉Γ ⊆ ⤉Δ.
+Proof.
+  eapply map_fmap_mono.
+Qed.
+
+Lemma renaming_heap_ctx_inclusion Σ Σ' : Σ ⊆ Σ' → ⤉Σ ⊆ ⤉Σ'.
+Proof.
+  eapply map_fmap_mono.
+Qed.
+
+Lemma typed_weakening n m Γ Δ e A Σ Σ' :
+  TY Σ; n; Γ ⊢ e : A →
+  Γ ⊆ Δ →
+  Σ ⊆ Σ' →
+  n ≤ m →
+  TY Σ'; m; Δ ⊢ e : A.
+Proof.
+  induction 1 as [| Σ n Γ x e A B Htyp IH | | Σ n Γ e A Htyp IH | | | Σ n Γ A B e e' x Hwf H1 IH1 H2 IH2 | | | | | | | | |  | | | | | | | Σ n Γ l A Hlook | | | ] in Σ', Δ, m |-*; intros Hsub1 Hsub2 Hle; eauto using type_wf_mono.
+  - (* var *) econstructor. by eapply lookup_weaken.
+  - (* lam *) econstructor; last by eapply type_wf_mono. eapply IH; eauto. by eapply insert_mono.
+  - (* tlam *) econstructor. eapply IH; last by lia.
+    + by eapply renaming_ctx_inclusion.
+    + by eapply renaming_heap_ctx_inclusion.
+  - (* pack *)
+    econstructor; last naive_solver. all: (eapply type_wf_mono; [ done | lia]).
+  - (* unpack *) econstructor.
+    + eapply type_wf_mono; done.
+    + eapply IH1; done.
+    + eapply IH2; last lia.
+      * apply insert_mono. by apply renaming_ctx_inclusion.
+      * by apply renaming_heap_ctx_inclusion.
+  - (* loc *)
+    econstructor; by eapply lookup_weaken.
+Qed.
+
+Lemma type_wf_subst_dom σ τ n A:
+  type_wf n A →
+  (∀ m, m < n → σ m = τ m) →
+  A.[σ] = A.[τ].
+Proof.
+  induction 1 in σ, τ |-*; simpl; eauto.
+  - (* tforall *)
+    intros Heq; asimpl. f_equal.
+    eapply IHtype_wf; intros [|m]; rewrite /up; simpl; first done.
+    intros Hlt. f_equal. eapply Heq. lia.
+  - (* texists *)
+    intros Heq; asimpl. f_equal.
+    eapply IHtype_wf. intros [ | m]; rewrite /up; simpl; first done.
+    intros Hlt. f_equal. apply Heq. lia.
+  - (* fun *) intros ?. f_equal; eauto.
+  - (* prod *) intros ?. f_equal; eauto.
+  - (* sum *) intros ?. f_equal; eauto.
+  - (* rec *)
+    intros Heq; asimpl. f_equal.
+    eapply IHtype_wf; intros [|m]; rewrite /up; simpl; first done.
+    intros Hlt. f_equal. eapply Heq. lia.
+  - (* ref *)
+    intros ?. f_equal. eapply IHtype_wf. done.
+Qed.
+
+Lemma type_wf_closed A σ:
+  type_wf 0 A →
+  A.[σ] = A.
+Proof.
+  intros Hwf; erewrite (type_wf_subst_dom _ (ids) 0).
+  - by asimpl.
+  - done.
+  - intros ??; lia.
+Qed.
+
+Lemma heap_ctx_closed Σ σ:
+  heap_ctx_wf 0 Σ →
+  fmap (subst σ) Σ = Σ.
+Proof.
+  intros Hwf. eapply stdpp.fin_maps.map_eq; intros l.
+  rewrite lookup_fmap. destruct lookup as [A|]eqn: H; last done; simpl.
+  f_equal. eapply type_wf_closed. by eapply Hwf.
+Qed.
+
+
+
+(** Typing inversion lemmas *)
+Lemma var_inversion Σ Γ n (x: string) A: TY Σ; n; Γ ⊢ x : A → Γ !! x = Some A.
+Proof. inversion 1; subst; auto. Qed.
+
+Lemma lam_inversion Σ n Γ (x: string) e C:
+  TY Σ; n; Γ ⊢ (λ: x, e) : C →
+  ∃ A B, C = (A → B)%ty ∧ type_wf n A ∧ TY Σ; n; <[x:=A]> Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma lam_anon_inversion Σ n Γ e C:
+  TY Σ; n; Γ ⊢ (λ: <>, e) : C →
+  ∃ A B, C = (A → B)%ty ∧ type_wf n A ∧ TY Σ; n; Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma app_inversion Σ n Γ e1 e2 B:
+  TY Σ; n; Γ ⊢ e1 e2 : B →
+  ∃ A, TY Σ; n; Γ ⊢ e1 : (A → B) ∧ TY Σ; n; Γ ⊢ e2 : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma if_inversion Σ n Γ e0 e1 e2 B:
+  TY Σ; n; Γ ⊢ If e0 e1 e2 : B →
+  TY Σ; n; Γ ⊢ e0 : Bool ∧ TY Σ; n; Γ ⊢ e1 : B ∧ TY Σ; n; Γ ⊢ e2 : B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma binop_inversion Σ n Γ op e1 e2 B:
+  TY Σ; n; Γ ⊢ BinOp op e1 e2 : B →
+  ∃ A1 A2, bin_op_typed op A1 A2 B ∧ TY Σ; n; Γ ⊢ e1 : A1 ∧ TY Σ; n; Γ ⊢ e2 : A2.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma unop_inversion Σ n Γ op e B:
+  TY Σ; n; Γ ⊢ UnOp op e : B →
+  ∃ A, un_op_typed op A B ∧ TY Σ; n; Γ ⊢ e : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma type_app_inversion Σ n Γ e B:
+  TY Σ; n; Γ ⊢ e <> : B →
+  ∃ A C, B = A.[C/] ∧ type_wf n C ∧ TY Σ; n; Γ ⊢ e : (∀: A).
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma type_lam_inversion Σ n Γ e B:
+  TY Σ; n; Γ ⊢ (Λ,e) : B →
+  ∃ A, B = (∀: A)%ty ∧ TY ⤉Σ; (S n); ⤉Γ ⊢ e : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma type_pack_inversion Σ n Γ e B :
+  TY Σ; n; Γ ⊢ (pack e) : B →
+  ∃ A C, B = (∃: A)%ty ∧ TY Σ; n; Γ ⊢ e : (A.[C/])%ty ∧ type_wf n C ∧ type_wf (S n) A.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma type_unpack_inversion Σ n Γ e e' x B :
+  TY Σ; n; Γ ⊢ (unpack e as x in e') : B →
+  ∃ A x', x = BNamed x' ∧ type_wf n B ∧ TY Σ; n; Γ ⊢ e : (∃: A) ∧ TY ⤉Σ; S n; <[x' := A]> (⤉Γ) ⊢ e' : (B.[ren (+1)]).
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma pair_inversion Σ n Γ e1 e2 C :
+  TY Σ; n; Γ ⊢ (e1, e2) : C →
+  ∃ A B, C = (A × B)%ty ∧ TY Σ; n; Γ ⊢ e1 : A ∧ TY Σ; n; Γ ⊢ e2 : B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma fst_inversion Σ n Γ e A :
+  TY Σ; n; Γ ⊢ Fst e : A →
+  ∃ B, TY Σ; n; Γ ⊢ e : A × B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma snd_inversion Σ n Γ e B :
+  TY Σ; n; Γ ⊢ Snd e : B →
+  ∃ A, TY Σ; n; Γ ⊢ e : A × B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma injl_inversion Σ n Γ e C :
+  TY Σ; n; Γ ⊢ InjL e : C →
+  ∃ A B, C = (A + B)%ty ∧ TY Σ; n; Γ ⊢ e : A ∧ type_wf n B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma injr_inversion Σ n Γ e C :
+  TY Σ; n; Γ ⊢ InjR e : C →
+  ∃ A B, C = (A + B)%ty ∧ TY Σ; n; Γ ⊢ e : B ∧ type_wf n A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma case_inversion Σ n Γ e e1 e2 A :
+  TY Σ; n; Γ ⊢ Case e e1 e2 : A →
+  ∃ B C, TY Σ; n; Γ ⊢ e : B + C ∧ TY Σ; n; Γ ⊢ e1 : (B → A) ∧ TY Σ; n; Γ ⊢ e2 : (C → A).
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma roll_inversion Σ n Γ e B:
+  TY Σ; n; Γ ⊢ (roll e) : B →
+  ∃ A, B = (μ: A)%ty ∧ TY Σ; n; Γ ⊢ e : A.[μ: A/].
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma unroll_inversion Σ n Γ e B:
+  TY Σ; n; Γ ⊢ (unroll e) : B →
+  ∃ A, B = (A.[μ: A/])%ty ∧ TY Σ; n; Γ ⊢ e : μ: A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma new_inversion Σ n Γ e B :
+  TY Σ; n; Γ ⊢ (new e) : B →
+  ∃ A, B = Ref A ∧ TY Σ; n; Γ ⊢ e : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma load_inversion Σ n Γ e B:
+  TY Σ; n; Γ ⊢ ! e : B →
+  TY Σ; n; Γ ⊢ e : Ref B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma store_inversion Σ n Γ e1 e2 B:
+  TY Σ; n; Γ ⊢ (e1 <- e2) : B →
+  ∃ A, B = Unit ∧ TY Σ; n; Γ ⊢ e1 : Ref A ∧ TY Σ; n; Γ ⊢ e2 : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma typed_substitutivity Σ n e e' Γ (x: string) A B :
+  heap_ctx_wf 0 Σ →
+  TY Σ; 0; ∅ ⊢ e' : A →
+  TY Σ; n; (<[x := A]> Γ) ⊢ e : B →
+  TY Σ; n; Γ ⊢ lang.subst x e' e : B.
+Proof.
+  intros HwfΣ He'. induction e as [| y | y | | | | | | | | | | | | | | | | | | | ] in n, B, Γ |-*; simpl.
+  - inversion 1; subst; auto.
+  - intros Hp % var_inversion.
+    destruct (decide (x = y)).
+    + subst. rewrite lookup_insert in Hp. injection Hp as ->.
+      eapply typed_weakening; [done| | done |lia]. apply map_empty_subseteq.
+    + rewrite lookup_insert_ne in Hp; last done. auto.
+  - destruct y as [ | y].
+    { intros (A' & C & -> & Hwf & Hty) % lam_anon_inversion.
+      econstructor; last done. destruct decide as [Heq|].
+      + congruence.
+      + eauto.
+    }
+    intros (A' & C & -> & Hwf & Hty) % lam_inversion.
+    econstructor; last done. destruct decide as [Heq|].
+    + injection Heq as [= ->]. by rewrite insert_insert in Hty.
+    + rewrite insert_commute in Hty; last naive_solver. eauto.
+  - intros (C & Hty1 & Hty2) % app_inversion. eauto.
+  - intros (? & Hop & H1) % unop_inversion.
+    destruct op; inversion Hop; subst; eauto.
+  - intros (? & ? & Hop & H1 & H2) % binop_inversion.
+    destruct op; inversion Hop; subst; eauto.
+  - intros (H1 & H2 & H3)%if_inversion. naive_solver.
+  - intros (C & D & -> & Hwf & Hty) % type_app_inversion. eauto.
+  - intros (C & -> & Hty)%type_lam_inversion. econstructor.
+    rewrite heap_ctx_closed //=.
+    eapply IHe. revert Hty. rewrite fmap_insert.
+    eapply syn_typed_wf in He'; eauto.
+    rewrite heap_ctx_closed //=.
+    rewrite type_wf_closed; eauto.
+  - intros (C & D & -> & Hty & Hwf1 & Hwf2)%type_pack_inversion.
+    econstructor; [done..|]. apply IHe. done.
+  - intros (C & x' & -> & Hwf & Hty1 & Hty2)%type_unpack_inversion.
+    econstructor; first done.
+    + eapply IHe1. done.
+    + destruct decide as [Heq | ].
+      * injection Heq as [= ->]. by rewrite fmap_insert insert_insert in Hty2.
+      * rewrite fmap_insert in Hty2. rewrite insert_commute in Hty2; last naive_solver.
+        revert Hty2. rewrite heap_ctx_closed//=. intros Hty2.
+        eapply IHe2. rewrite type_wf_closed in Hty2; first done.
+        eapply syn_typed_wf; last apply He'; eauto.
+  - intros (? & ? & -> & ? & ?) % pair_inversion. eauto.
+  - intros (? & ?)%fst_inversion. eauto.
+  - intros (? & ?)%snd_inversion. eauto.
+  - intros (? & ? & -> & ? & ?)%injl_inversion. eauto.
+  - intros (? & ? & -> & ? & ?)%injr_inversion. eauto.
+  - intros (? & ? & ? & ? & ?)%case_inversion. eauto.
+  - intros (C & -> & Hty) % roll_inversion. eauto.
+  - intros (C & -> & Hty) % unroll_inversion. eauto.
+  - intros Hty % load_inversion. eauto.
+  - intros (C & -> & Hty1 & Hty2)% store_inversion. eauto.
+  - intros (C & -> & Hty) % new_inversion. eauto.
+Qed.
+
+(** Canonical values *)
+Lemma canonical_values_arr Σ n Γ e A B:
+  TY Σ; n; Γ ⊢ e : (A → B) →
+  is_val e →
+  ∃ x e', e = (λ: x, e')%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_forall Σ n Γ e A:
+  TY Σ; n; Γ ⊢ e : (∀: A)%ty →
+  is_val e →
+  ∃ e', e = (Λ, e')%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_exists Σ n Γ e A :
+  TY Σ; n; Γ ⊢ e : (∃: A) →
+  is_val e →
+  ∃ e', e = (pack e')%E.
+Proof. inversion 1; simpl; naive_solver. Qed.
+
+Lemma canonical_values_int Σ n Γ e:
+  TY Σ; n; Γ ⊢ e : Int →
+  is_val e →
+  ∃ n: Z, e = (#n)%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_bool Σ n Γ e:
+  TY Σ; n; Γ ⊢ e : Bool →
+  is_val e →
+  ∃ b: bool, e = (#b)%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_unit Σ n Γ e:
+  TY Σ; n; Γ ⊢ e : Unit →
+  is_val e →
+  e = (#LitUnit)%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_prod Σ n Γ e A B :
+  TY Σ; n; Γ ⊢ e : A × B →
+  is_val e →
+  ∃ e1 e2, e = (e1, e2)%E ∧ is_val e1 ∧ is_val e2.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_sum Σ n Γ e A B :
+  TY Σ; n; Γ ⊢ e : A + B →
+  is_val e →
+  (∃ e', e = InjL e' ∧ is_val e') ∨ (∃ e', e = InjR e' ∧ is_val e').
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_rec Σ n Γ e A:
+  TY Σ; n; Γ ⊢ e : (μ: A) →
+  is_val e →
+  ∃ e', e = (roll e')%E ∧ is_val e'.
+Proof.
+  inversion 1; simpl; subst; naive_solver.
+Qed.
+
+Lemma canonical_values_ref Σ n Γ e A:
+  TY Σ; n; Γ ⊢ e : Ref A →
+  is_val e →
+  ∃ l: loc, e = (#l)%E ∧ Σ !! l = Some A.
+Proof.
+  inversion 1; simpl; subst; naive_solver.
+Qed.
+
+(** Progress *)
+Definition heap_type (h: heap) Σ :=
+  ∀ l A, Σ !! l = Some A → ∃ v, h !! l = Some v ∧ TY Σ; 0; ∅ ⊢ of_val v : A.
+
+Lemma typed_progress Σ e h A:
+  heap_type h Σ →
+  TY Σ; 0; ∅ ⊢ e : A →
+  is_val e ∨ reducible e h.
+Proof.
+  intros Hheap. remember ∅ as Γ. remember 0 as n.
+  induction 1 as [| | | | Σ n Γ A B e Hty IH | Σ n Γ A B e Hwf Hwf' Hty IH | Σ n Γ A B e e' x Hwf Hty1 IH1 Hty2 IH2 | | | | Σ n Γ e0 e1 e2 A Hty1 IH1 Hty2 IH2 Hty3 IH3 | Σ n Γ e1 e2 A B Hty IH1 _ IH2 | Σ n Γ e1 e2 op A B C Hop Hty1 IH1 Hty2 IH2 | Σ n Γ e op A B Hop Hty IH | Σ n Γ e1 e2 A B Hty1 IH1 Hty2 IH2 | Σ n Γ e A B Hty IH | Σ n Γ e A B Hty IH | Σ n Γ e A B Hwf Hty IH | Σ n Γ e A B Hwf Hty IH| Σ n Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2 | Σ n Γ e A Hty IH | Σ n Γ e A Hty IH | Σ n Γ l A Hlook | Σ n Γ e A Hty IH | Σ n Γ e1 e2 A Hty1 IH1 Hty2 IH2 | Σ n Γ e A Hty IH ].
+  - subst. naive_solver.
+  - left. done.
+  - left. done.
+  - left; done.
+  - right. destruct (IH Hheap HeqΓ Heqn) as [H1|H1].
+    + eapply canonical_values_forall in Hty as [e' ->]; last done.
+      eexists _, _. eapply base_contextual_step. eapply TBetaS.
+    + destruct H1 as (e' & h' & H1). eexists _, _.
+      eapply (fill_contextual_step [TAppCtx]). done.
+  - (* pack *)
+    destruct (IH Hheap HeqΓ Heqn) as [H | H].
+    + by left.
+    + right. destruct H as (e' & h' & H). eexists _, _. eapply (fill_contextual_step [PackCtx]). done.
+  - (* unpack *)
+    destruct (IH1 Hheap HeqΓ Heqn) as [H | H].
+    + eapply canonical_values_exists in Hty1 as [e'' ->]; last done.
+      right. eexists _, _. eapply base_contextual_step. constructor; last done.
+      done.
+    + right. destruct H as (e'' & h'' & H). eexists _, _.
+      eapply (fill_contextual_step [UnpackCtx _ _]). done.
+  - (* int *)left. done.
+  - (* bool*) left. done.
+  - (* unit *) left. done.
+  - (* if *)
+    destruct (IH1 Hheap HeqΓ Heqn) as [H1 | H1].
+    + eapply canonical_values_bool in Hty1 as (b & ->); last done.
+      right. destruct b; eexists _, _; eapply base_contextual_step; constructor.
+    + right. destruct H1 as (e0' & h' & Hstep).
+      eexists _, _. by eapply (fill_contextual_step [IfCtx _ _]).
+  - (* app *)
+    destruct (IH2 Hheap HeqΓ Heqn) as [H2|H2]; [destruct (IH1 Hheap HeqΓ Heqn) as [H1|H1]|].
+    + eapply canonical_values_arr in Hty as (x & e & ->); last done.
+      right. eexists _, _.
+      eapply base_contextual_step, BetaS; eauto.
+    + right. eapply is_val_spec in H2 as [v Heq].
+      replace e2 with (of_val v); last by eapply of_to_val.
+      destruct H1 as (e1' & h' & Hstep).
+      eexists _, _. eapply (fill_contextual_step [AppLCtx v]). done.
+    + right. destruct H2 as (e2' & h' & H2).
+      eexists _, _. eapply (fill_contextual_step [AppRCtx e1]). done.
+  - (* binop *)
+    assert (A = Int ∧ B = Int) as [-> ->].
+    { inversion Hop; subst A B C; done. }
+    destruct (IH2 Hheap HeqΓ Heqn) as [H2|H2]; [destruct (IH1 Hheap HeqΓ Heqn) as [H1|H1]|].
+    + right. eapply canonical_values_int in Hty1 as [n1 ->]; last done.
+      eapply canonical_values_int in Hty2 as [n2 ->]; last done.
+      inversion Hop; subst; simpl.
+      all: eexists _, _; eapply base_contextual_step; eapply BinOpS; eauto.
+    + right. eapply is_val_spec in H2 as [v Heq].
+      replace e2 with (of_val v); last by eapply of_to_val.
+      destruct H1 as (e1' & h' & Hstep).
+      eexists _, _. eapply (fill_contextual_step [BinOpLCtx op v]). done.
+    + right. destruct H2 as (e2' & h' & H2).
+      eexists _, _. eapply (fill_contextual_step [BinOpRCtx op e1]). done.
+  - (* unop *)
+    inversion Hop; subst A B op.
+    + right. destruct (IH Hheap HeqΓ Heqn) as [H2 | H2].
+      * eapply canonical_values_bool in Hty as [b ->]; last done.
+        eexists _, _; eapply base_contextual_step; eapply UnOpS; eauto.
+      * destruct H2 as (e' & h' & H2). eexists _, _.
+        eapply (fill_contextual_step [UnOpCtx _]). done.
+    + right. destruct (IH Hheap HeqΓ Heqn) as [H2 | H2].
+      * eapply canonical_values_int in Hty as [z ->]; last done.
+        eexists _, _; eapply base_contextual_step; eapply UnOpS; eauto.
+      * destruct H2 as (e' & h' & H2). eexists _, _.
+        eapply (fill_contextual_step [UnOpCtx _]). done.
+  - (* pair *)
+    destruct (IH2 Hheap HeqΓ Heqn) as [H2|H2]; [destruct (IH1 Hheap HeqΓ Heqn) as [H1|H1]|].
+    + left. done.
+    + right. eapply is_val_spec in H2 as [v Heq].
+      replace e2 with (of_val v); last by eapply of_to_val.
+      destruct H1 as (e1' & h' & Hstep).
+      eexists _, _. eapply (fill_contextual_step [PairLCtx v]). done.
+    + right. destruct H2 as (e2' & h' & H2).
+      eexists _, _. eapply (fill_contextual_step [PairRCtx e1]). done.
+  - (* fst *)
+    destruct (IH Hheap HeqΓ Heqn) as [H | H].
+    + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done.
+      right. eexists _, _. eapply base_contextual_step. econstructor; done.
+    + right. destruct H as (e' & h' & H).
+      eexists _, _. eapply (fill_contextual_step [FstCtx]). done.
+  - (* snd *)
+    destruct (IH Hheap HeqΓ Heqn) as [H | H].
+    + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done.
+      right. eexists _, _. eapply base_contextual_step. econstructor; done.
+    + right. destruct H as (e' & h' & H).
+      eexists _, _. eapply (fill_contextual_step [SndCtx]). done.
+  - (* injl *)
+    destruct (IH Hheap HeqΓ Heqn) as [H | H].
+    + left. done.
+    + right. destruct H as (e' & h' & H).
+      eexists _, _. eapply (fill_contextual_step [InjLCtx]). done.
+  - (* injr *)
+    destruct (IH Hheap HeqΓ Heqn) as [H | H].
+    + left. done.
+    + right. destruct H as (e' & h' & H).
+      eexists _, _. eapply (fill_contextual_step [InjRCtx]). done.
+  - (* case *)
+    right. destruct (IHe Hheap HeqΓ Heqn) as [H1|H1].
+    + eapply canonical_values_sum in Htye as [(e' & -> & ?) | (e' & -> & ?)]; last done.
+      * eexists _, _. eapply base_contextual_step. econstructor. done.
+      * eexists _, _. eapply base_contextual_step. econstructor. done.
+    + destruct H1 as (e' & h' & H1). eexists _, _.
+      eapply (fill_contextual_step [CaseCtx e1 e2]). done.
+  - (* roll *)
+    destruct (IH Hheap HeqΓ Heqn) as [Hval|Hred].
+    + by left.
+    + right. destruct Hred as (e' & h' & Hred).
+      eexists _, _. eapply (fill_contextual_step [RollCtx]). done.
+  - (* unroll *)
+    destruct (IH Hheap HeqΓ Heqn) as [Hval|Hred].
+    + eapply canonical_values_rec in Hty as (e' & -> & Hval'); last done.
+      right. eexists _, _. eapply base_contextual_step. by econstructor.
+    + right. destruct Hred as (e' & h' & Hred).
+      eexists _, _. eapply (fill_contextual_step [UnrollCtx]). done.
+  - (* loc *)
+    by left.
+  - (* load *)
+    destruct (IH Hheap HeqΓ Heqn) as [Hval|Hred].
+    + eapply canonical_values_ref in Hty as (l & -> & Hlook); last done.
+      eapply Hheap in Hlook as (v & Hlook & Hty').
+      right. do 2 eexists. eapply base_contextual_step. by econstructor.
+    + right. destruct Hred as (e' & h' & Hred).
+      do 2 eexists. eapply (fill_contextual_step [LoadCtx]). done.
+  - (* store *)
+    destruct (IH2 Hheap HeqΓ Heqn) as [H2|H2]; [destruct (IH1 Hheap HeqΓ Heqn) as [H1|H1]|].
+    + right. eapply canonical_values_ref in Hty1 as (l & -> & Hlook); last done.
+      eapply Hheap in Hlook as (v & Hlook & Hty').
+      eapply is_val_spec in H2 as (w & Heq).
+      do 2 eexists. eapply base_contextual_step.
+      econstructor; eauto.
+    + right. eapply is_val_spec in H2 as [v Heq].
+      replace e2 with (of_val v); last by eapply of_to_val.
+      destruct H1 as (e1' & h' & Hstep).
+      do 2 eexists. eapply (fill_contextual_step [StoreLCtx v]). done.
+    + right. destruct H2 as (e2' & h' & H2).
+      do 2 eexists. eapply (fill_contextual_step [StoreRCtx e1]). done.
+  - (* new *)
+    destruct (IH Hheap HeqΓ Heqn) as [Hval|Hred].
+    + right. eapply is_val_spec in Hval as [v Heq].
+      do 2 eexists. eapply base_contextual_step.
+      eapply (NewS _ _ _ (fresh (dom h))); last done.
+      eapply not_elem_of_dom, is_fresh.
+    + right. destruct Hred as (e' & h' & Hred).
+      do 2 eexists. eapply (fill_contextual_step [NewCtx]). done.
+Qed.
+
+Definition ectx_item_typing Σ (K: ectx_item) (A B: type) :=
+  ∀ e Σ', Σ ⊆ Σ' → TY Σ'; 0; ∅ ⊢ e : A → TY Σ'; 0; ∅ ⊢ (fill_item K e) : B.
+
+Notation ectx := (list ectx_item).
+Definition ectx_typing Σ (K: ectx) (A B: type) :=
+  ∀ e Σ', Σ ⊆ Σ' → TY Σ'; 0; ∅ ⊢ e : A → TY Σ'; 0; ∅ ⊢ (fill K e) : B.
+
+Lemma ectx_item_typing_weaking Σ Σ' k B A :
+  Σ ⊆ Σ' → ectx_item_typing Σ k B A → ectx_item_typing Σ' k B A.
+Proof.
+  intros Hsub Hty e Σ'' Hsub'' Hty'. eapply Hty; last done.
+  by transitivity Σ'.
+Qed.
+
+Lemma ectx_typing_weaking Σ Σ' K B A :
+  Σ ⊆ Σ' → ectx_typing Σ K B A → ectx_typing Σ' K B A.
+Proof.
+  intros Hsub Hty e Σ'' Hsub'' Hty'. eapply Hty; last done.
+  by transitivity Σ'.
+Qed.
+
+Lemma fill_item_typing_decompose Σ k e A:
+  TY Σ; 0; ∅ ⊢ fill_item k e : A →
+  ∃ B, TY Σ; 0; ∅ ⊢ e : B ∧ ectx_item_typing Σ k B A.
+Proof.
+  unfold ectx_item_typing; destruct k; simpl; inversion 1; subst; eauto 6 using typed_weakening, map_fmap_mono.
+Qed.
+
+Lemma fill_typing_decompose Σ K e A:
+  TY Σ; 0; ∅ ⊢ fill K e : A →
+  ∃ B, TY Σ; 0; ∅ ⊢ e : B ∧ ectx_typing Σ K B A.
+Proof.
+  unfold ectx_typing; revert e; induction K as [|k K]; intros e; simpl; eauto.
+  intros [B [Hit Hty]] % IHK.
+  eapply fill_item_typing_decompose in Hit as [B' [? ?]]; eauto.
+Qed.
+
+Lemma fill_typing_compose Σ K e A B:
+  TY Σ; 0; ∅ ⊢ e : B →
+  ectx_typing Σ K B A →
+  TY Σ; 0; ∅ ⊢ fill K e : A.
+Proof.
+  intros H1 H2; by eapply H2.
+Qed.
+
+Lemma fmap_up_subst_ctx σ Γ: ⤉(subst σ <$> Γ) = subst (up σ) <$> ⤉Γ.
+Proof.
+  rewrite -!map_fmap_compose.
+  eapply map_fmap_ext. intros x A _. by asimpl.
+Qed.
+
+Lemma fmap_up_subst_heap_ctx σ Σ: ⤉(subst σ <$> Σ) = subst (up σ) <$> ⤉Σ.
+Proof.
+  rewrite -!map_fmap_compose.
+  eapply map_fmap_ext. intros x A _. by asimpl.
+Qed.
+
+Lemma typed_subst_type Σ n m Γ e A σ:
+  TY Σ; n; Γ ⊢ e : A → (∀ k, k < n → type_wf m (σ k)) → TY (subst σ) <$> Σ; m; (subst σ) <$> Γ ⊢ e : A.[σ].
+Proof.
+  induction 1 as [ Σ n Γ x A Heq | | | Σ n Γ e A Hty IH | | Σ n Γ A B e Hwf Hwf' Hty IH | Σ n Γ A B e e' x Hwf Hty1 IH1 Hty2 IH2 | | | | | |? ? ? ? ? ? ? ? ? Hop | ? ? ? ? ? ? ? Hop | | | | | | | |  | | | | ] in σ, m |-*; simpl; intros Hlt; eauto.
+  - econstructor. rewrite lookup_fmap Heq //=.
+  - econstructor; last by eapply type_wf_subst.
+    rewrite -fmap_insert. eauto.
+  - econstructor; last by eapply type_wf_subst. eauto.
+  - econstructor. rewrite fmap_up_subst_ctx fmap_up_subst_heap_ctx. eapply IH.
+    intros [| x] Hlt'; rewrite /up //=.
+    + econstructor. lia.
+    + eapply type_wf_rename; last by (intros ???; simpl; lia).
+      eapply Hlt. lia.
+  - replace (A.[B/].[σ]) with (A.[up σ].[B.[σ]/]) by by asimpl.
+    eauto using type_wf_subst.
+  - (* pack *)
+    eapply (typed_pack _ _ _ _ (subst σ B)).
+    + eapply type_wf_subst; done.
+    + eapply type_wf_subst; first done.
+      intros [ | k] Hk; first ( asimpl;constructor; lia).
+      rewrite /up //=. eapply type_wf_rename; last by (intros ???; simpl; lia).
+      eapply Hlt. lia.
+    + replace (A.[up σ].[B.[σ]/]) with (A.[B/].[σ])  by by asimpl.
+      eauto using type_wf_subst.
+  - (* unpack *)
+    eapply (typed_unpack _ _ _ A.[up σ]).
+    + eapply type_wf_subst; done.
+    + replace (∃: A.[up σ])%ty with ((∃: A).[σ])%ty by by asimpl.
+      eapply IH1. done.
+    + rewrite fmap_up_subst_ctx fmap_up_subst_heap_ctx. rewrite -fmap_insert.
+      replace (B.[σ].[ren (+1)]) with (B.[ren(+1)].[up σ]) by by asimpl.
+      eapply IH2.
+      intros [ | k] Hk; asimpl; first (constructor; lia).
+      eapply type_wf_subst; first (eapply Hlt; lia).
+      intros k' Hk'. asimpl. constructor. lia.
+  - (* binop *)
+    inversion Hop; subst.
+    all: econstructor; naive_solver.
+  - (* unop *)
+    inversion Hop; subst.
+    all: econstructor; naive_solver.
+  - econstructor; last naive_solver. by eapply type_wf_subst.
+  - econstructor; last naive_solver. by eapply type_wf_subst.
+  - (* roll *)
+    econstructor.
+    replace (A.[up σ].[μ: A.[up σ]/])%ty with (A.[μ: A/].[σ])%ty by by asimpl. eauto.
+  - (* unroll *)
+    replace (A.[μ: A/].[σ])%ty with (A.[up σ].[μ: A.[up σ]/])%ty by by asimpl.
+    econstructor. eapply IHsyn_typed. done.
+  - (* loc *)
+    econstructor. rewrite lookup_fmap H //=.
+Qed.
+
+Lemma typed_subst_type_closed Σ C e A:
+  type_wf 0 C →
+  heap_ctx_wf 0 Σ →
+  TY ⤉Σ; 1; ⤉∅ ⊢ e : A → TY Σ; 0; ∅ ⊢ e : A.[C/].
+Proof.
+  intros Hwf Hwf' Hty. eapply typed_subst_type with (σ := C .: ids) (m := 0) in Hty; last first.
+  { intros [|k] Hlt; last lia. done. }
+  revert Hty. rewrite !fmap_empty.
+  rewrite !(heap_ctx_closed Σ); eauto.
+Qed.
+
+Lemma typed_subst_type_closed' Σ x C B e A:
+  type_wf 0 A →
+  type_wf 1 C →
+  type_wf 0 B →
+  heap_ctx_wf 0 Σ →
+  TY ⤉Σ; 1; <[x := C]> ∅ ⊢ e : A →
+  TY Σ; 0; <[x := C.[B/]]> ∅ ⊢ e : A.
+Proof.
+  intros ???? Hty.
+  set (s := (subst (B.:ids))).
+  rewrite -(fmap_empty s) -(fmap_insert s).
+  replace A with (A.[B/]).
+  2: { replace A with (A.[ids]) at 2 by by asimpl.
+      eapply type_wf_subst_dom; first done. lia.
+  }
+  rewrite -(heap_ctx_closed Σ (B.:ids)); last done.
+  eapply typed_subst_type.
+  { rewrite -(heap_ctx_closed Σ (ren (+1))); done. }
+  intros [ | k] Hk; last lia. done.
+Qed.
+
+Lemma heap_ctx_insert h l A Σ:
+  heap_type h Σ → h !! l = None → Σ ⊆ <[l:=A]> Σ.
+Proof.
+  intros Hheap Hlook. eapply insert_subseteq.
+  specialize (Hheap l). destruct (lookup) as [B|]; last done.
+  specialize (Hheap B eq_refl) as (w & Hsome & _). congruence.
+Qed.
+
+Lemma heap_type_insert h Σ e v l B :
+  heap_type h Σ →
+  h !! l = None →
+  TY Σ; 0; ∅ ⊢ e : B →
+  to_val e = Some v →
+  heap_type ({[l := v]} ∪ h) (<[l:=B]> Σ).
+Proof.
+  intros Hheap Hlook Hty Hval l' A. rewrite lookup_insert_Some.
+  intros [(-> & ->)|(Hne & Hlook')].
+  - exists v. split; first eapply lookup_union_Some_l, lookup_insert.
+    eapply of_to_val in Hval as ->.
+    eapply typed_weakening; first eapply Hty; eauto.
+    by eapply heap_ctx_insert.
+  - eapply Hheap in Hlook' as (w & Hlook' & Hty').
+    eexists; split.
+    + rewrite lookup_union_r; eauto.
+      rewrite lookup_insert_ne //=.
+    + eapply typed_weakening; first eapply Hty'; eauto.
+      by eapply heap_ctx_insert.
+Qed.
+
+Lemma heap_type_update h Σ e v l B :
+  heap_type h Σ →
+  Σ !! l = Some B →
+  TY Σ; 0; ∅ ⊢ e : B →
+  to_val e = Some v →
+  heap_type (<[l:=v]> h) Σ.
+Proof.
+  intros Hheap Hlook Hty Hval l' A Hlook'.
+  eapply Hheap in Hlook' as Hlook''.
+  destruct Hlook'' as (w & Hold & Hval').
+  destruct (decide (l = l')); subst.
+  - exists v. split; first eapply lookup_insert.
+    eapply of_to_val in Hval as ->.
+    rewrite Hlook in Hlook'. by injection Hlook' as ->.
+  - rewrite lookup_insert_ne //=. eauto.
+Qed.
+
+
+
+Lemma typed_preservation_base_step Σ e e' h h' A:
+  heap_ctx_wf 0 Σ →
+  TY Σ; 0; ∅ ⊢ e : A →
+  heap_type h Σ →
+  base_step (e, h) (e', h') →
+  ∃ Σ', Σ ⊆ Σ' ∧ heap_type h' Σ' ∧ heap_ctx_wf 0 Σ' ∧ TY Σ'; 0; ∅ ⊢ e' : A.
+Proof.
+  intros Hwf' Hty Hhty Hstep. inversion Hstep as [ | | | op e1 v v' h1 Heq Heval | op e1 v1 e2 v2 v3 h1 Heq1 Heq2 Heval | | |  | | | | | | | ]; subst.
+  - eapply app_inversion in Hty as (B & H1 & H2).
+    destruct x as [|x].
+    { eapply lam_anon_inversion in H1 as (C & D & [= -> ->] & Hwf & Hty).
+      exists Σ. do 3 (split; first done). done. }
+    eapply lam_inversion in H1 as (C & D & Heq & Hwf & Hty).
+    injection Heq as -> ->.
+    exists Σ. do 3 (split; first done).
+    eapply typed_substitutivity; eauto.
+  - eapply type_app_inversion in Hty as (B & C & -> & Hwf & Hty).
+    eapply type_lam_inversion in Hty as (A & Heq & Hty).
+    injection Heq as ->. exists Σ. split_and!; [done.. | ]. by eapply typed_subst_type_closed.
+  - eapply type_unpack_inversion in Hty as (B & x' & -> & Hwf & Hty1 & Hty2).
+    eapply type_pack_inversion in Hty1 as (B' & C & [= <-] & Hty1 & ? & ?).
+    exists Σ. split_and!; [done.. | ].
+    eapply typed_substitutivity.
+    { done. }
+    { apply Hty1. }
+    rewrite fmap_empty in Hty2.
+    eapply typed_subst_type_closed'; eauto.
+    replace A with A.[ids] by by asimpl.
+    enough (A.[ids] = A.[ren (+1)]) as -> by done.
+    eapply type_wf_subst_dom; first done. intros; lia.
+  - (* unop *)
+    eapply unop_inversion in Hty as (A1 & Hop & Hty).
+    assert ((A1 = Int ∧ A = Int) ∨ (A1 = Bool ∧ A = Bool)) as [(-> & ->) | (-> & ->)].
+    { inversion Hop; subst; eauto. }
+    + eapply canonical_values_int in Hty as [n ->]; last by eapply is_val_spec; eauto.
+      simpl in Heq. injection Heq as <-.
+      exists Σ; split_and!; [done..|].
+      inversion Hop; subst; simpl in *; injection Heval as <-; constructor.
+    + eapply canonical_values_bool in Hty as [b ->]; last by eapply is_val_spec; eauto.
+      simpl in Heq. injection Heq as <-.
+      exists Σ; split_and!; [done..|].
+      inversion Hop; subst; simpl in *; injection Heval as <-; constructor.
+  - (* binop *)
+    eapply binop_inversion in Hty as (A1 & A2 & Hop & Hty1 & Hty2).
+    assert (A1 = Int ∧ A2 = Int ∧ (A = Int ∨ A = Bool)) as (-> & -> & HC).
+    { inversion Hop; subst; eauto. }
+    eapply canonical_values_int in Hty1 as [n ->]; last by eapply is_val_spec; eauto.
+    eapply canonical_values_int in Hty2 as [m ->]; last by eapply is_val_spec; eauto.
+    simpl in Heq1, Heq2. injection Heq1 as <-. injection Heq2 as <-.
+    simpl in Heval.
+    exists Σ; split_and!; [done..|].
+    inversion Hop; subst; simpl in *; injection Heval as <-; constructor.
+  - exists Σ; split_and!; [done..|].
+    by eapply if_inversion in Hty as (H1 & H2 & H3).
+  - exists Σ; split_and!; [done..|].
+    by eapply if_inversion in Hty as (H1 & H2 & H3).
+  - exists Σ; split_and!; [done..|].
+    by eapply fst_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion).
+  - exists Σ; split_and!; [done..|].
+    by eapply snd_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion).
+  - exists Σ; split_and!; [done..|].
+    eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty & ?)%injl_inversion & ? & ?).
+    eauto.
+  - exists Σ; split_and!; [done..|].
+    eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty & ?)%injr_inversion & ? & ?).
+    eauto.
+  - (* unroll *)
+    exists Σ; split_and!; [done..|].
+    eapply unroll_inversion in Hty as (B & -> & Hty).
+    eapply roll_inversion in Hty as (C & Heq & Hty). injection Heq as ->. done.
+  
+- (* new *)
+    eapply new_inversion in Hty as (B & -> & Hty).
+    exists (<[l := B]> Σ). repeat split.
+    + by eapply heap_ctx_insert.
+    + rewrite /init_heap; simpl; rewrite right_id.
+      by eapply heap_type_insert.
+    + eapply heap_ctx_wf_insert; first done.
+      eapply syn_typed_wf; eauto.
+    + econstructor. by rewrite lookup_insert.
+  - (* load *)
+    exists Σ. do 3 (split; first done).
+    eapply load_inversion in Hty.
+    eapply canonical_values_ref in Hty as (l' & Heq & Hlook); last done.
+    injection Heq as <-. eapply Hhty in Hlook as (w & Hlook & Hty).
+    naive_solver.
+  - (* store *)
+    eapply store_inversion in Hty as (B & -> & Hty1 & Hty2).
+    exists Σ. repeat split; try eauto.
+    eapply heap_type_update; eauto. inversion Hty1; subst; done. 
+Qed.
+
+Lemma typed_preservation Σ e e' h h' A:
+  heap_ctx_wf 0 Σ →
+  TY Σ; 0; ∅ ⊢ e : A →
+  heap_type h Σ →
+  contextual_step (e, h) (e', h') →
+  ∃ Σ', Σ ⊆ Σ' ∧ heap_type h' Σ' ∧ heap_ctx_wf 0 Σ' ∧ TY Σ'; 0; ∅ ⊢ e' : A.
+Proof.
+  intros Hwf Hty Hheap Hstep. inversion Hstep as [K e1' e2' σ1 σ2 e1 e2 -> -> Hstep']; subst.
+  eapply fill_typing_decompose in Hty as [B [H1 H2]].
+  eapply typed_preservation_base_step in H1 as (Σ' & Hsub & Hheap' & Hwf' & Hty'); eauto.
+  eexists; repeat split; try done.
+  eapply fill_typing_compose, ectx_typing_weaking; eauto.
+Qed.
+
+Lemma typed_preservation_steps Σ e e' h h' A:
+  heap_ctx_wf 0 Σ →
+  TY Σ; 0; ∅ ⊢ e : A →
+  heap_type h Σ →
+  rtc contextual_step (e, h) (e', h') →
+  ∃ Σ', Σ ⊆ Σ' ∧ heap_type h' Σ' ∧ heap_ctx_wf 0 Σ' ∧ TY Σ'; 0; ∅ ⊢ e' : A.
+Proof.
+  intros Hwf Hty Hheap Hsteps. remember (e, h) as c1. remember (e', h') as c2.
+  induction Hsteps as [|? [] ? Hstep Hsteps IH] in Σ, h, h',e, e', Heqc1, Heqc2, Hwf, Hty, Hheap |-*.
+  - rewrite Heqc1 in Heqc2. injection Heqc2 as -> ->. eauto.
+  - subst; eapply typed_preservation in Hty as (Σ' & Hsub' & Hheap' & Hwf' & Hty'); [|eauto..].
+    eapply IH in Hty' as (Σ'' & Hsub'' & Hheap'' & Hwf'' & Hty''); [|eauto..].
+    exists Σ''; repeat split; eauto. by trans Σ'.
+Qed.
+
+Lemma type_safety Σ e1 e2 h1 h2 A:
+  heap_ctx_wf 0 Σ →
+  TY Σ; 0; ∅ ⊢ e1 : A →
+  heap_type h1 Σ →
+  rtc contextual_step (e1, h1) (e2, h2) →
+  is_val e2 ∨ reducible e2 h2.
+Proof.
+  intros Hwf Hy Hheap Hsteps.
+  eapply typed_preservation_steps in Hsteps as (Σ' & Hsub & Hheap' & Hwf' & Hty'); eauto.
+  eapply typed_progress; eauto.
+Qed.
+
+(* applies to terms containing no free locations (like the erasure of source terms) *)
+Corollary closed_type_safety e e' h A:
+  TY ∅; 0; ∅ ⊢ e : A →
+  rtc contextual_step (e, ∅) (e', h) →
+  is_val e' ∨ reducible e' h.
+Proof.
+  intros Hty Hsteps. eapply type_safety; eauto.
+  intros ??. set_solver.
+Qed.
+
+(** Derived typing rules *)
+Lemma typed_unroll' Σ n Γ e A B:
+  TY Σ; n; Γ ⊢ e : (μ: A) →
+  B = A.[(μ: A)%ty/] →
+  TY Σ; n; Γ ⊢ (unroll e) : B.
+Proof.
+  intros ? ->. by eapply typed_unroll.
+Qed.
+
+Lemma typed_tapp' Σ n Γ A B C e :
+  TY Σ; n; Γ ⊢ e : (∀: A) →
+  type_wf n B →
+  C = A.[B/] →
+  TY Σ; n; Γ ⊢ e <> : C.
+Proof.
+ intros; subst C; by eapply typed_tapp.
+Qed.