diff --git a/_CoqProject b/_CoqProject
index c4576c1..e621d45 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -57,9 +57,21 @@ theories/type_systems/systemf_mu/notation.v
 theories/type_systems/systemf_mu/types.v
 theories/type_systems/systemf_mu/tactics.v
 theories/type_systems/systemf_mu/pure.v
+theories/type_systems/systemf_mu/pure_sol.v
 theories/type_systems/systemf_mu/untyped_encoding.v
 theories/type_systems/systemf_mu/parallel_subst.v
 theories/type_systems/systemf_mu/logrel.v
+theories/type_systems/systemf_mu/logrel_sol.v
+
+# SystemF + Mu + State
+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/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
 
 # By removing the # below, you can add the exercise sheets to make
 #theories/type_systems/warmup/warmup.v
@@ -77,3 +89,5 @@ theories/type_systems/systemf_mu/logrel.v
 #theories/type_systems/systemf/exercises05.v
 #theories/type_systems/systemf/exercises05_sol.v
 #theories/type_systems/systemf_mu/exercises06.v
+#theories/type_systems/systemf_mu/exercises06_sol.v
+#theories/type_systems/systemf_mu_state/exercises07.v
diff --git a/theories/type_systems/systemf_mu_state/execution.v b/theories/type_systems/systemf_mu_state/execution.v
new file mode 100644
index 0000000..d63a9da
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/execution.v
@@ -0,0 +1,450 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.ts.systemf_mu_state Require Import lang notation.
+(* TODO: everywhere replace the metavar σ for heaps with h *)
+
+(** ** Deterministic reduction *)
+
+Record det_step (e1 : expr) (e2 : expr) := {
+  det_step_safe h : reducible e1 h;
+  det_step_det e2' h h' :
+    contextual_step (e1, h) (e2', h') → e2' = e2 ∧ h' = h
+}.
+
+Record det_base_step (e1 e2 : expr) := {
+  det_base_step_safe h : base_reducible e1 h;
+  det_base_step_det e2' h h' :
+    base_step (e1, h) (e2', h') → e2' = e2 ∧ h' = h
+}.
+
+Lemma det_base_step_det_step e1 e2 : det_base_step e1 e2 → det_step e1 e2.
+Proof.
+  intros [Hp1 Hp2]. split.
+  - intros h. destruct (Hp1 h) as (e2' & h' & ?).
+    eexists e2', h'. by apply base_contextual_step.
+  - intros e2' h h' ?%base_reducible_contextual_step; [ | done]. by eapply Hp2.
+Qed.
+
+(** *** Pure execution lemmas *)
+Local Ltac inv_step :=
+  repeat match goal with
+  | H : to_val _ = Some _ |- _ => apply of_to_val in H
+  | H : base_step (?e, ?σ) (?e2, ?σ2) |- _ =>
+     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
+     and should thus better be avoided. *)
+     inversion H; subst; clear H
+  end.
+Local Ltac solve_exec_safe := intros; subst; eexists _, _; econstructor; eauto.
+Local Ltac solve_exec_detdet := simpl; intros; inv_step; try done.
+Local Ltac solve_det_exec :=
+  subst; intros; apply det_base_step_det_step;
+    constructor; [solve_exec_safe | solve_exec_detdet].
+
+Lemma det_step_beta x e e2 :
+  is_val e2 →
+  det_step (App (@Lam x e) e2) (subst' x e2 e).
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_tbeta e :
+  det_step ((Λ, e) <>) e.
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_unpack e1 e2 x :
+  is_val e1 →
+  det_step (unpack (pack e1) as x in e2) (subst' x e1 e2).
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_unop op e v v' :
+  to_val e = Some v →
+  un_op_eval op v = Some v' →
+  det_step (UnOp op e) v'.
+Proof. solve_det_exec. by simplify_eq. Qed.
+
+Lemma det_step_binop op e1 v1 e2 v2 v' :
+  to_val e1 = Some v1 →
+  to_val e2 = Some v2 →
+  bin_op_eval op v1 v2 = Some v' →
+  det_step (BinOp op e1 e2) v'.
+Proof. solve_det_exec. by simplify_eq. Qed.
+
+Lemma det_step_if_true e1 e2 :
+  det_step (if: #true then e1 else e2) e1.
+Proof. solve_det_exec. Qed.
+Lemma det_step_if_false e1 e2 :
+  det_step (if: #false then e1 else e2) e2.
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_fst e1 e2 :
+  is_val e1 →
+  is_val e2 →
+  det_step (Fst (e1, e2)) e1.
+Proof. solve_det_exec. Qed.
+Lemma det_step_snd e1 e2 :
+  is_val e1 →
+  is_val e2 →
+  det_step (Snd (e1, e2)) e2.
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_casel e e1 e2 :
+  is_val e →
+  det_step (Case (InjL e) e1 e2) (e1 e).
+Proof. solve_det_exec. Qed.
+Lemma det_step_caser e e1 e2 :
+  is_val e →
+  det_step (Case (InjR e) e1 e2) (e2 e).
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_unroll e :
+  is_val e →
+  det_step (unroll (roll e)) e.
+Proof. solve_det_exec. Qed.
+
+(** ** n-step reduction *)
+(** Reduce in n steps to an irreducible expression.
+    (this is ⇝^n from the lecture notes)
+ *)
+Definition red_nsteps (n : nat) e h e' h' := nsteps contextual_step n (e, h) (e', h') ∧ irreducible e' h'.
+
+Lemma det_step_red e e' e'' h h'' n :
+  det_step e e' →
+  red_nsteps n e h e'' h'' →
+  1 ≤ n ∧ red_nsteps (n - 1) e' h e'' h''.
+Proof.
+  intros [Hprog Hstep] Hred.
+  specialize (Hprog h).
+  destruct Hred as [Hred  Hirred].
+  destruct n as [ | n].
+  { inversion Hred; subst.
+    exfalso; eapply not_reducible; done.
+  }
+  inversion Hred as [ | ??[e1 h1]? Hstep0]; subst. simpl.
+  apply Hstep in Hstep0 as [<- <-].
+  split; first lia.
+  replace (n - 0) with n by lia. done.
+Qed.
+
+Lemma contextual_step_red_nsteps n e e' e'' h h' h'':
+  contextual_step (e, h) (e', h') →
+  red_nsteps n e' h' e'' h'' →
+  red_nsteps (S n) e h e'' h''.
+Proof.
+  intros Hstep [Hsteps Hirred].
+  split; last done.
+  by econstructor.
+Qed.
+
+Lemma nsteps_val_inv n v e' h h' :
+  red_nsteps n (of_val v) h e' h' → n = 0 ∧ e' = of_val v ∧ h' = h.
+Proof.
+  intros [Hred Hirred]; cbn in *.
+  destruct n as [ | n].
+  - inversion Hred; subst. done.
+  - inversion Hred as [ | ??[e1 h1]]; subst. exfalso. eapply val_irreducible; last done.
+    rewrite to_of_val. eauto.
+Qed.
+
+Lemma nsteps_val_inv' n v e e' h h' :
+  to_val e = Some v →
+  red_nsteps n e h e' h' → n = 0 ∧ e' = of_val v ∧ h' = h.
+Proof. intros Ht. rewrite -(of_to_val _ _ Ht). apply nsteps_val_inv. Qed.
+
+Lemma red_nsteps_fill K k e e' h h' :
+  red_nsteps k (fill K e) h e' h' →
+  ∃ j e'' h'', j ≤ k ∧
+    red_nsteps j e h e'' h'' ∧
+    red_nsteps (k - j) (fill K e'') h'' e' h'.
+Proof.
+  intros [Hsteps Hirred].
+  induction k as [ | k IH] in e, e', h, h', Hsteps, Hirred |-*.
+  - inversion Hsteps; subst.
+    exists 0, e, h'. split_and!; [done | split | ].
+    + constructor.
+    + by eapply irreducible_fill.
+    + done.
+  - inversion Hsteps as [ | n [e1 h1] [e2 h2] [e3 h3] Hstep Hsteps' Heq1 Heq2 Heq3]. subst.
+    destruct (contextual_ectx_step_case _ _ _ _ _ Hstep) as [(e'' & -> & Hstep') | Hv].
+    + apply IH in Hsteps' as (j & e3 & h3 & ? & Hsteps' & Hsteps''); last done.
+      eexists (S j), _, _. split_and!; [lia | | done ].
+      eapply contextual_step_red_nsteps; done.
+    + exists 0, e, h. split_and!; [ lia | | ].
+      * split; [constructor | ].
+        apply val_irreducible. by apply is_val_spec.
+      * simpl. by eapply contextual_step_red_nsteps.
+Qed.
+
+(** * Heap execution lemmas *)
+Lemma new_step_inv v e e' σ σ' :
+  to_val e = Some v →
+  base_step (New e, σ) (e', σ') →
+  ∃ l, e' = (Lit $ LitLoc l) ∧ σ' = init_heap l 1 v σ ∧ σ !! l = None.
+Proof.
+  intros <-%of_to_val.
+  inversion 1; subst.
+  rewrite to_of_val in H5. injection H5 as [= ->].
+  eauto.
+Qed.
+
+Lemma new_nsteps_inv n v e e' σ σ' :
+  to_val e = Some v →
+  red_nsteps n (New e) σ e' σ' →
+  (n = 1 ∧ base_step (New e, σ) (e', σ')).
+Proof.
+  intros <-%of_to_val [Hsteps Hirred%not_reducible].
+  inversion Hsteps; subst.
+  - exfalso; apply Hirred. eapply base_reducible_reducible. eexists _, _. eapply new_fresh.
+  - destruct y.
+    eapply base_reducible_contextual_step in H.
+    2: { eexists _, _. apply new_fresh. }
+    inversion H0; subst.
+    { eauto. }
+    eapply new_step_inv in H; last apply to_of_val.
+    destruct H as (l & -> & -> & ?).
+    destruct y. apply val_stuck in H1. done.
+Qed.
+
+Lemma load_step_inv e v σ e' σ' :
+  to_val e = Some v →
+  base_step (Load e, σ) (e', σ') →
+  ∃ (l : loc) v', v = #l ∧ σ !! l = Some v' ∧ e' = of_val v' ∧ σ' = σ.
+Proof.
+  intros <-%of_to_val.
+  inversion 1; subst.
+  symmetry in H0. apply of_val_lit in H0 as ->.
+  eauto 8.
+Qed.
+
+Definition sub_redexes_are_values (e : expr) :=
+    ∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx.
+
+Lemma contextual_base_reducible e σ :
+  reducible e σ → sub_redexes_are_values e → base_reducible e σ.
+Proof.
+  intros (e' & σ' & Hstep) ?. inversion Hstep; subst.
+  assert (K = empty_ectx) as -> by eauto 10 using val_base_stuck.
+  rewrite fill_empty /base_reducible; eauto.
+Qed.
+
+
+Ltac solve_sub_redexes_are_values :=
+  let K := fresh "K" in
+  let e' := fresh "e'" in
+  let Heq := fresh "Heq" in
+  let Hv := fresh "Hv" in
+  let IH := fresh "IH" in
+  let Ki := fresh "Ki" in
+  let Ki' := fresh "Ki'" in
+  intros K e' Heq Hv;
+  destruct K as [ | Ki K]; first (done);
+  exfalso; induction K as [ | Ki' K IH] in e', Ki, Hv, Heq |-*;
+  [destruct Ki; inversion Heq; subst; simplify_val; cbn in *; congruence
+  | eapply IH; first (by rewrite Heq);
+    apply fill_item_no_val; done].
+
+Lemma load_nsteps_inv n v e e' σ σ' :
+  to_val e = Some v →
+  red_nsteps n (Load e) σ e' σ' →
+  (n = 0 ∧ σ' = σ ∧ e' = Load e ∧ ¬ reducible (Load e) σ) ∨
+  (n = 1 ∧ base_step (Load e, σ) (e', σ')).
+Proof.
+  intros <-%of_to_val [Hsteps Hirred%not_reducible].
+  inversion Hsteps; subst.
+  - by left.
+  - right. destruct y.
+    eapply base_reducible_contextual_step in H.
+    2: { eapply contextual_base_reducible; [eexists _, _; done | solve_sub_redexes_are_values]. }
+    inversion H0; subst.
+    { eauto. }
+    eapply load_step_inv in H as (l & ? & -> & ? & -> & ->); last apply to_of_val.
+    destruct y. apply val_stuck in H1. simplify_val. done.
+Qed.
+
+(** useful derived lemma when we know upfront that l satisfies some invariant [P] *)
+Lemma load_nsteps_inv' n l e e' σ σ' (P : val → Prop) :
+  to_val e = Some (LitV $ LitLoc l) →
+  (∃ v', σ !! l = Some v' ∧ P v') →
+  red_nsteps n (Load e) σ e' σ' →
+  ∃ v' : val, n = 1 ∧ e' = v' ∧ σ' = σ ∧ σ !! l = Some v' ∧ P v'.
+Proof.
+  intros <-%of_to_val (v' & Hlook & HP) Hred.
+  eapply load_nsteps_inv in Hred; last done.
+  destruct Hred as [(-> & -> & -> & Hnred) | (-> & Hstep)].
+  - exfalso; eapply Hnred. eexists v', _.
+    eapply base_contextual_step. econstructor. done.
+  - exists v'. split; first done.
+    eapply load_step_inv in Hstep; last done.
+    destruct Hstep as (l' & v'' & [= <-] & ? & -> & ->).
+    split; first by simplify_option_eq.
+    split; last done. econstructor; done.
+Qed.
+
+Lemma store_step_inv v1 v2 σ e' σ' :
+  base_step (Store (of_val v1) (of_val v2), σ) (e', σ') →
+  ∃ (l : loc) v', v1 = #l ∧ σ !! l = Some v' ∧ e' = Lit LitUnit ∧ σ' = <[l := v2]> σ.
+Proof.
+  inversion 1; subst.
+  symmetry in H0. apply of_val_lit in H0 as ->.
+  simplify_val. simplify_option_eq.
+  eauto 8.
+Qed.
+
+Lemma store_nsteps_inv n v1 v2 e' σ σ' :
+  red_nsteps n (Store (of_val v1) (of_val v2)) σ e' σ' →
+  (n = 0 ∧ σ' = σ ∧ e' = Store (of_val v1) (of_val v2) ∧ ¬ reducible (Store (of_val v1) (of_val v2)) σ) ∨
+  (n = 1 ∧ base_step (Store (of_val v1) (of_val v2), σ) (e', σ')).
+Proof.
+  intros [Hsteps Hirred%not_reducible].
+  inversion Hsteps; subst.
+  - by left.
+  - right. destruct y.
+    eapply base_reducible_contextual_step in H.
+    2: { eapply contextual_base_reducible; [eexists _, _; done | solve_sub_redexes_are_values]. }
+    inversion H0; subst.
+    { eauto. }
+    apply store_step_inv in H as (l & ? & -> & ? & -> & ->).
+    destruct y. apply val_stuck in H1. simplify_val. done.
+Qed.
+
+Lemma store_nsteps_inv' n e1 e2 v0 v l e' σ σ' :
+  to_val e1 = Some (LitV $ LitLoc l) →
+  to_val e2 = Some v →
+  σ !! l = Some v0 →
+  red_nsteps n (Store e1 e2) σ e' σ' →
+  n = 1 ∧ e' = Lit $ LitUnit ∧ σ' = <[l := v ]> σ.
+Proof.
+  intros <-%of_to_val <-%of_to_val Hlook Hred%store_nsteps_inv.
+  destruct Hred as [(-> & -> & -> & Hnred) | (-> & Hb)].
+  - exfalso; eapply Hnred.
+    eexists #(), _.
+    eapply base_contextual_step. econstructor; [done | apply to_of_val ].
+  - eapply store_step_inv in Hb. destruct Hb as (l' & v' & [= <-] & Hlook' & -> & ->).
+    simplify_option_eq. done.
+Qed.
+
+(** Additionally useful stepping lemmas *)
+Lemma app_step_r (e1 e2 e2': expr) h h' :
+  contextual_step (e2, h) (e2', h') → contextual_step (e1 e2, h) (e1 e2', h').
+Proof. by apply (fill_contextual_step [AppRCtx _]). Qed.
+
+Lemma app_step_l (e1 e1' e2: expr) h h' :
+  contextual_step (e1, h) (e1', h') → is_val e2 → contextual_step (e1 e2, h) (e1' e2, h').
+Proof.
+  intros ? (v & Hv)%is_val_spec.
+  rewrite <-(of_to_val _ _ Hv).
+  by apply (fill_contextual_step [AppLCtx _]).
+Qed.
+
+Lemma app_step_beta (x: string) (e e': expr) h :
+  is_val e' → is_closed [x] e → contextual_step ((λ: x, e)%E e', h) (lang.subst x e' e, h).
+Proof.
+  intros Hval Hclosed. eapply base_contextual_step, BetaS; eauto.
+Qed.
+
+Lemma unroll_roll_step (e: expr) h :
+  is_val e → contextual_step ((unroll (roll e))%E, h) (e, h).
+Proof.
+  intros ?; by eapply base_contextual_step, UnrollS.
+Qed.
+
+Lemma fill_reducible K e h : 
+  reducible e h → reducible (fill K e) h.
+Proof.
+  intros (e' & h' & Hstep).
+  exists (fill K e'), h'. eapply fill_contextual_step. done.
+Qed.
+
+Lemma reducible_contextual_step_case K e e' h1 h2 :
+  contextual_step (fill K e, h1) (e', h2) → 
+  reducible e h1 →
+  ∃ e'', e' = fill K e'' ∧ contextual_step (e, h1) (e'', h2).
+Proof.
+  intros [ | Hval]%contextual_ectx_step_case Hred; first done.
+  exfalso. apply is_val_spec in Hval as (v & Hval). 
+  apply reducible_not_val in Hred. congruence.
+Qed.
+
+(** Contextual lifting lemmas for deterministic reduction *)
+Tactic Notation "lift_det" uconstr(ctx) := 
+  intros; 
+  let Hs := fresh in 
+  match goal with 
+  | H : det_step _ _ |- _ => destruct H as [? Hs]
+  end;
+  simplify_val; econstructor; 
+  [intros; by eapply (fill_reducible ctx) | 
+   intros ? ? ? (? & -> & [-> ->]%Hs)%(reducible_contextual_step_case ctx); done ].
+
+Lemma det_step_pair_r e1 e2 e2' :
+  det_step e2 e2' →
+  det_step (e1, e2)%E (e1, e2')%E.
+Proof. lift_det [PairRCtx _]. Qed.
+
+Lemma det_step_pair_l e1 e1' e2 :
+  is_val e2 →
+  det_step e1 e1' →
+  det_step (e1, e2)%E (e1', e2)%E.
+Proof. lift_det [PairLCtx _]. Qed.
+Lemma det_step_binop_r e1 e2 e2' op :
+  det_step e2 e2' →
+  det_step (BinOp op e1 e2)%E (BinOp op e1 e2')%E.
+Proof. lift_det [BinOpRCtx _ _]. Qed.
+Lemma det_step_binop_l e1 e1' e2 op :
+  is_val e2 →
+  det_step e1 e1' →
+  det_step (BinOp op e1 e2)%E (BinOp op e1' e2)%E.
+Proof. lift_det [BinOpLCtx _ _]. Qed.
+Lemma det_step_if e e' e1 e2 :
+  det_step e e' →
+  det_step (If e e1 e2)%E (If e' e1 e2)%E.
+Proof. lift_det [IfCtx _ _]. Qed.
+Lemma det_step_app_r e1 e2 e2' :
+  det_step e2 e2' →
+  det_step (App e1 e2)%E (App e1 e2')%E.
+Proof. lift_det [AppRCtx _]. Qed.
+Lemma det_step_app_l e1 e1' e2 :
+  is_val e2 →
+  det_step e1 e1' →
+  det_step (App e1 e2)%E (App e1' e2)%E.
+Proof. lift_det [AppLCtx _]. Qed.
+Lemma det_step_snd_lift e e' :
+  det_step e e' →
+  det_step (Snd e)%E (Snd e')%E.
+Proof. lift_det [SndCtx]. Qed.
+Lemma det_step_fst_lift e e' :
+  det_step e e' →
+  det_step (Fst e)%E (Fst e')%E.
+Proof. lift_det [FstCtx]. Qed.
+Lemma det_step_store_r e1 e2 e2' :
+  det_step e2 e2' →
+  det_step (Store e1 e2)%E (Store e1 e2')%E.
+Proof. lift_det [StoreRCtx _]. Qed.
+Lemma det_step_store_l e1 e1' e2 :
+  is_val e2 →
+  det_step e1 e1' →
+  det_step (Store e1 e2)%E (Store e1' e2)%E.
+Proof. lift_det [StoreLCtx _]. Qed.
+
+
+#[global]
+Hint Resolve app_step_r app_step_l app_step_beta unroll_roll_step : core.
+#[global]
+Hint Extern 1 (is_val _) => (simpl; fast_done) : core.
+#[global]
+Hint Immediate is_val_of_val : core.
+
+#[global]
+Hint Resolve det_step_beta det_step_tbeta det_step_unpack det_step_unop det_step_binop det_step_if_true det_step_if_false det_step_fst det_step_snd det_step_casel det_step_caser det_step_unroll : core.
+
+#[global]
+Hint Resolve det_step_pair_r det_step_pair_l det_step_binop_r det_step_binop_l det_step_if det_step_app_r det_step_app_l det_step_snd_lift det_step_fst_lift det_step_store_l det_step_store_r : core.
+
+#[global]
+Hint Constructors nsteps : core.
+
+#[global] 
+Hint Extern 1 (is_val _) => simpl : core.
+
+Ltac do_det_step :=
+  match goal with 
+  | |- nsteps det_step _ _ _ => econstructor 2; first do_det_step
+  | |- det_step _ _ => simpl; solve[eauto 10]
+  end.
diff --git a/theories/type_systems/systemf_mu_state/exercises07.v b/theories/type_systems/systemf_mu_state/exercises07.v
new file mode 100644
index 0000000..59c2d19
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/exercises07.v
@@ -0,0 +1,127 @@
+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", #0. (* FIXME *)
+  
+
+Definition make_mystack : val :=
+  Λ, λ: "lc",
+    unpack "lc" as "lc" in
+    #0. (* FIXME *)
+
+Lemma make_mystack_typed Σ n Γ :
+  TY Σ; n; Γ ⊢ make_mystack : (∀: list_t #0 → stack_t #0).
+Proof.
+  repeat solve_typing_fast.
+Admitted.
+
+
+(** 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 #0 (* FIXME: what is the result? *), h').
+Proof.
+  eexists. unfold obf_expr.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+(** Exercise 4 (LN Exercise 48): Fibonacci *)
+
+
+Definition fibonacci : val := #0. (* FIXME *)
+  
+Lemma fibonacci_typed Σ n Γ :
+  TY Σ; n; Γ ⊢ fibonacci : (Int → Int).
+Proof.
+  repeat solve_typing_fast.
+Admitted.
diff --git a/theories/type_systems/systemf_mu_state/lang.v b/theories/type_systems/systemf_mu_state/lang.v
new file mode 100644
index 0000000..fc0a055
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/lang.v
@@ -0,0 +1,858 @@
+From iris.prelude Require Import prelude.
+From stdpp Require Export binders strings.
+From semantics.ts.systemf_mu_state Require Export locations.
+From semantics.lib Require Export maps.
+
+Declare Scope expr_scope.
+Declare Scope val_scope.
+Delimit Scope expr_scope with E.
+Delimit Scope val_scope with V.
+
+(** Expressions and vals. *)
+Inductive base_lit : Set :=
+  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
+Inductive un_op : Set :=
+  | NegOp | MinusUnOp.
+Inductive bin_op : Set :=
+  | PlusOp | MinusOp | MultOp (* Arithmetic *)
+  | LtOp | LeOp | EqOp. (* Comparison *)
+
+
+Inductive expr :=
+  | Lit (l : base_lit)
+  (* Base lambda calculus *)
+  | Var (x : string)
+  | Lam (x : binder) (e : expr)
+  | App (e1 e2 : expr)
+  (* Base types and their operations *)
+  | UnOp (op : un_op) (e : expr)
+  | BinOp (op : bin_op) (e1 e2 : expr)
+  | If (e0 e1 e2 : expr)
+  (* Polymorphism *)
+  | TApp (e : expr)
+  | TLam (e : expr)
+  | Pack (e : expr)
+  | Unpack (x : binder) (e1 e2 : expr)
+  (* Products *)
+  | Pair (e1 e2 : expr)
+  | Fst (e : expr)
+  | Snd (e : expr)
+  (* Sums *)
+  | InjL (e : expr)
+  | InjR (e : expr)
+  | Case (e0 : expr) (e1 : expr) (e2 : expr)
+  (* Isorecursive types *)
+  | Roll (e : expr)
+  | Unroll (e : expr)
+  (* State *)
+  | Load (e : expr)
+  | Store (e1 e2 : expr)
+  | New (e : expr)
+.
+
+Bind Scope expr_scope with expr.
+
+Inductive val :=
+  | LitV (l : base_lit)
+  | LamV (x : binder) (e : expr)
+  | TLamV (e : expr)
+  | PackV (v : val)
+  | PairV (v1 v2 : val)
+  | InjLV (v : val)
+  | InjRV (v : val)
+  | RollV (v : val)
+.
+
+Bind Scope val_scope with val.
+
+Fixpoint of_val (v : val) : expr :=
+  match v with
+  | LitV l => Lit l
+  | LamV x e => Lam x e
+  | TLamV e => TLam e
+  | PackV v => Pack (of_val v)
+  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
+  | InjLV v => InjL (of_val v)
+  | InjRV v => InjR (of_val v)
+  | RollV v => Roll (of_val v)
+  end.
+
+Fixpoint to_val (e : expr) : option val :=
+  match e with
+  | Lit l => Some $ LitV l
+  | Lam x e => Some (LamV x e)
+  | TLam e => Some (TLamV e)
+  | Pack e =>
+     to_val e ≫= (λ v, Some $ PackV v)
+  | Pair e1 e2 =>
+    to_val e1 ≫= (λ v1, to_val e2 ≫= (λ v2, Some $ PairV v1 v2))
+  | InjL e => to_val e ≫= (λ v, Some $ InjLV v)
+  | InjR e => to_val e ≫= (λ v, Some $ InjRV v)
+  | Roll e => to_val e ≫= (λ v, Some $ RollV v)
+  | _ => None
+  end.
+
+(** Equality and other typeclass stuff *)
+Lemma to_of_val v : to_val (of_val v) = Some v.
+Proof.
+  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
+Qed.
+
+Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+Proof.
+  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
+Qed.
+
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
+Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
+
+(** structural computational version *)
+Fixpoint is_val (e : expr) : Prop :=
+  match e with
+  | Lit l => True
+  | Lam x e => True
+  | TLam e => True
+  | Pack e => is_val e
+  | Pair e1 e2 => is_val e1 ∧ is_val e2
+  | InjL e => is_val e
+  | InjR e => is_val e
+  | Roll e => is_val e
+  | _ => False
+  end.
+Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
+Proof.
+  induction e as [ | | ? e IH | e1 IH1 e2 IH2 | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 | e IH | e IH | e IH | e IH | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | | | ];
+    simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try naive_solver.
+  - rewrite IH. intros (v & ->). eauto.
+  - rewrite IH1 IH2. intros [(v1 & ->) (v2 & ->)]. eauto.
+  - rewrite IH. intros (v & ->). eauto.
+  - rewrite IH. intros (v & ->); eauto.
+  - rewrite IH. intros (v & ->). eauto.
+Qed.
+
+Global Instance base_lit_eq_dec : EqDecision base_lit.
+Proof. solve_decision. Defined.
+Global Instance un_op_eq_dec : EqDecision un_op.
+Proof. solve_decision. Defined.
+Global Instance bin_op_eq_dec : EqDecision bin_op.
+Proof. solve_decision. Defined.
+
+
+(** Substitution *)
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | Lit _ => e
+  | Var y => if decide (x = y) then es else Var y
+  | Lam y e =>
+      Lam y $ if decide (BNamed x = y) then e else subst x es e
+  | App e1 e2 => App (subst x es e1) (subst x es e2)
+  | TApp e => TApp (subst x es e)
+  | TLam e => TLam (subst x es e)
+  | Pack e => Pack (subst x es e)
+  | Unpack y e1 e2 => Unpack y (subst x es e1) (if decide (BNamed x = y) then e2 else subst x es e2)
+  | UnOp op e => UnOp op (subst x es e)
+  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
+  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
+  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
+  | Fst e => Fst (subst x es e)
+  | Snd e => Snd (subst x es e)
+  | InjL e => InjL (subst x es e)
+  | InjR e => InjR (subst x es e)
+  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
+  | Roll e => Roll (subst x es e)
+  | Unroll e => Unroll (subst x es e)
+  | Load e => Load (subst x es e)
+  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
+  | New e => New (subst x es e)
+  end.
+
+Definition subst' (mx : binder) (es : expr) : expr → expr :=
+  match mx with BNamed x => subst x es | BAnon => id end.
+
+(** The stepping relation *)
+Definition un_op_eval (op : un_op) (v : val) : option val :=
+  match op, v with
+  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
+  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
+  | _, _ => None
+  end.
+
+Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
+  match op with
+  | PlusOp => Some $ LitInt (n1 + n2)
+  | MinusOp => Some $ LitInt (n1 - n2)
+  | MultOp => Some $ LitInt (n1 * n2)
+  | LtOp => Some $ LitBool (bool_decide (n1 < n2))
+  | LeOp => Some $ LitBool (bool_decide (n1 ≤ n2))
+  | EqOp => Some $ LitBool (bool_decide (n1 = n2))
+  end%Z.
+
+Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
+  match v1, v2 with
+  | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
+  | _, _ => None
+  end.
+
+Definition heap := gmap loc val.
+Fixpoint heap_array (l : loc) (vs : list val) : heap :=
+  match vs with
+  | [] => ∅
+  | v :: vs' => {[l := v]} ∪ heap_array (l +ₗ 1) vs'
+  end.
+
+Lemma heap_array_singleton l v : heap_array l [v] = {[l := v]}.
+Proof. by rewrite /heap_array right_id. Qed.
+
+Lemma heap_array_lookup l vs w k :
+  heap_array l vs !! k = Some w ↔
+  ∃ j, (0 ≤ j)%Z ∧ k = l +ₗ j ∧ vs !! (Z.to_nat j) = Some w.
+Proof.
+  revert k l; induction vs as [|v' vs IH]=> l' l /=.
+  { rewrite lookup_empty. naive_solver lia. }
+  rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
+  - intros [[-> ?] | (Hl & j & ? & -> & ?)].
+    { eexists 0. rewrite loc_add_0. naive_solver lia. }
+    eexists (1 + j)%Z. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; eauto with lia.
+  - intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
+    { rewrite loc_add_0. eauto. }
+    right. split.
+    { rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. }
+    assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
+    { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
+    rewrite Hj /= in Hil.
+    eexists (j - 1)%Z. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
+    auto with lia.
+Qed.
+
+Lemma heap_array_map_disjoint (h : heap) (l : loc) (vs : list val) :
+  (∀ i, (0 ≤ i)%Z → (i < length vs)%Z → h !! (l +ₗ i) = None) →
+  (heap_array l vs) ##ₘ h.
+Proof.
+  intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
+  intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
+  move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
+Qed.
+
+Definition init_heap (l : loc) (n : Z) (v : val) (σ : heap) : heap :=
+  heap_array l (replicate (Z.to_nat n) v) ∪ σ.
+
+Lemma init_heap_singleton l v σ :
+  init_heap l 1 v σ = <[l:=v]> σ.
+Proof.
+  rewrite /init_heap /=.
+  rewrite right_id insert_union_singleton_l. done.
+Qed.
+
+Inductive base_step : expr * heap → expr * heap → Prop :=
+  | BetaS x e1 e2 e' σ :
+     is_val e2 →
+     e' = subst' x e2 e1 →
+     base_step (App (Lam x e1) e2, σ) (e', σ)
+  | TBetaS e1 σ :
+      base_step (TApp (TLam e1), σ) (e1, σ)
+  | UnpackS e1 e2 e' x σ :
+      is_val e1 →
+      e' = subst' x e1 e2 →
+      base_step (Unpack x (Pack e1) e2, σ) (e', σ)
+  | UnOpS op e v v' σ :
+     to_val e = Some v →
+     un_op_eval op v = Some v' →
+     base_step (UnOp op e, σ) (of_val v', σ)
+  | BinOpS op e1 v1 e2 v2 v' σ :
+     to_val e1 = Some v1 →
+     to_val e2 = Some v2 →
+     bin_op_eval op v1 v2 = Some v' →
+     base_step (BinOp op e1 e2, σ) (of_val v', σ)
+  | IfTrueS e1 e2 σ :
+     base_step (If (Lit $ LitBool true) e1 e2, σ) (e1, σ)
+  | IfFalseS e1 e2 σ :
+     base_step (If (Lit $ LitBool false) e1 e2, σ) (e2, σ)
+  | FstS e1 e2 σ :
+     is_val e1 →
+     is_val e2 →
+     base_step (Fst (Pair e1 e2), σ) (e1, σ)
+  | SndS e1 e2 σ :
+     is_val e1 →
+     is_val e2 →
+     base_step (Snd (Pair e1 e2), σ) (e2, σ)
+  | CaseLS e e1 e2 σ :
+     is_val e →
+     base_step (Case (InjL e) e1 e2, σ) (App e1 e, σ)
+  | CaseRS e e1 e2 σ :
+     is_val e →
+     base_step (Case (InjR e) e1 e2, σ) (App e2 e, σ)
+  | UnrollS e σ :
+      is_val e →
+      base_step (Unroll (Roll e), σ) (e, σ)
+  | NewS e v σ l :
+     σ !! l = None →
+     to_val e = Some v →
+     base_step (New e, σ) (Lit $ LitLoc l, init_heap l 1 v σ)
+  | LoadS l v σ :
+     σ !! l = Some v →
+     base_step (Load (Lit $ LitLoc l), σ) (of_val v, σ)
+  | StoreS l v w e2 σ :
+     σ !! l = Some v →
+     to_val e2 = Some w →
+     base_step (Store (Lit $ LitLoc l) e2, σ)
+               (Lit LitUnit, <[l:=w]> σ)
+.
+
+(* Misc *)
+Lemma is_val_of_val v : is_val (of_val v).
+Proof. apply is_val_spec. rewrite to_of_val. eauto. Qed.
+
+(** If [e1] makes a base step to a value under some state [σ1] then any base
+ step from [e1] under any other state [σ1'] must necessarily be to a value. *)
+Lemma base_step_to_val e1 e2 e2' σ1 σ2 σ2' :
+  base_step (e1, σ1) (e2, σ2) →
+  base_step (e1, σ1) (e2', σ2') → is_Some (to_val e2) → is_Some (to_val e2').
+Proof. inversion 1; inversion 1; naive_solver. Qed.
+
+Lemma new_fresh v σ :
+  let l := fresh_locs (dom σ) in
+  base_step (New (of_val v), σ) (Lit $ LitLoc l, init_heap l 1 v σ).
+Proof.
+  intros.
+  apply NewS.
+  - apply (not_elem_of_dom).
+    rewrite -(loc_add_0 l).
+    by apply fresh_locs_fresh.
+  - rewrite to_of_val. eauto.
+Qed.
+
+(** We define evaluation contexts *)
+Inductive ectx_item :=
+  | AppLCtx (v2 : val)
+  | AppRCtx (e1 : expr)
+  | TAppCtx
+  | PackCtx
+  | UnpackCtx (x : binder) (e2 : expr)
+  | UnOpCtx (op : un_op)
+  | BinOpLCtx (op : bin_op) (v2 : val)
+  | BinOpRCtx (op : bin_op) (e1 : expr)
+  | IfCtx (e1 e2 : expr)
+  | PairLCtx (v2 : val)
+  | PairRCtx (e1 : expr)
+  | FstCtx
+  | SndCtx
+  | InjLCtx
+  | InjRCtx
+  | CaseCtx (e1 : expr) (e2 : expr)
+  | UnrollCtx
+  | RollCtx
+  | LoadCtx
+  | StoreRCtx (e1 : expr)
+  | StoreLCtx (v2 : val)
+  | NewCtx
+.
+
+Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
+  match Ki with
+  | AppLCtx v2 => App e (of_val v2)
+  | AppRCtx e1 => App e1 e
+  | TAppCtx => TApp e
+  | PackCtx => Pack e
+  | UnpackCtx x e2 => Unpack x e e2
+  | UnOpCtx op => UnOp op e
+  | BinOpLCtx op v2 => BinOp op e (of_val v2)
+  | BinOpRCtx op e1 => BinOp op e1 e
+  | IfCtx e1 e2 => If e e1 e2
+  | PairLCtx v2 => Pair e (of_val v2)
+  | PairRCtx e1 => Pair e1 e
+  | FstCtx => Fst e
+  | SndCtx => Snd e
+  | InjLCtx => InjL e
+  | InjRCtx => InjR e
+  | CaseCtx e1 e2 => Case e e1 e2
+  | UnrollCtx => Unroll e
+  | RollCtx => Roll e
+  | LoadCtx => Load e
+  | StoreRCtx e1 => Store e1 e
+  | StoreLCtx v2 => Store e (of_val v2)
+  | NewCtx => New e
+  end.
+
+(** Basic properties about the language *)
+Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
+
+Lemma fill_item_val Ki e :
+  is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
+Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed.
+Lemma fill_item_no_val Ki e :
+  to_val e = None → to_val (fill_item Ki e) = None.
+Proof.
+  intros Hn. destruct (to_val (fill_item _ _ )) eqn:Heq; last done.
+  edestruct (fill_item_val Ki e) as (? & ?); last simplify_eq.
+  eauto.
+Qed.
+
+Lemma val_base_stuck e1 e2 σ1 σ2 : base_step (e1, σ1) (e2, σ2) → to_val e1 = None.
+Proof. inversion 1; naive_solver. Qed.
+
+Lemma of_val_lit v l :
+  of_val v = (Lit l) → v = LitV l.
+Proof. destruct v; simpl; inversion 1; done. Qed.
+Lemma of_val_pair_inv (v v1 v2 : val) :
+  of_val v = Pair (of_val v1) (of_val v2) → v = PairV v1 v2.
+Proof.
+  destruct v; simpl; inversion 1.
+  apply of_val_inj in H1. apply of_val_inj in H2. subst; done.
+Qed.
+Lemma of_val_injl_inv (v v' : val) :
+  of_val v = InjL (of_val v') → v = InjLV v'.
+Proof.
+  destruct v; simpl; inversion 1.
+  apply of_val_inj in H1. subst; done.
+Qed.
+Lemma of_val_injr_inv (v v' : val) :
+  of_val v = InjR (of_val v') → v = InjRV v'.
+Proof.
+  destruct v; simpl; inversion 1.
+  apply of_val_inj in H1. subst; done.
+Qed.
+
+Ltac simplify_val :=
+  repeat match goal with
+  | H: to_val (of_val ?v) = ?o |- _ => rewrite to_of_val in H
+  | H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
+  | H: to_val ?e = ?v |- _ => is_var e; specialize (of_to_val _ _ H); intros <-; clear H
+  | H: of_val ?v = Lit ?l |- _ => is_var v; specialize (of_val_lit _ _ H); intros ->; clear H
+  | |- context[to_val (of_val ?e)] => rewrite to_of_val
+  end.
+Lemma base_ectxi_step_val Ki e e2 σ1 σ2 :
+  base_step (fill_item Ki e, σ1) (e2, σ2) → is_Some (to_val e).
+Proof.
+  revert e2. induction Ki; inversion_clear 1; simplify_option_eq; simplify_val; eauto.
+Qed.
+
+Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
+  to_val e1 = None → to_val e2 = None →
+  fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
+Proof.
+  revert Ki1. induction Ki2; intros Ki1; induction Ki1; try naive_solver eauto with f_equal.
+  all: intros ?? Heq; injection Heq; intros ??; simplify_eq; simplify_val; naive_solver.
+Qed.
+
+Section contexts.
+  Notation ectx := (list ectx_item).
+  Definition empty_ectx : ectx := [].
+  Definition comp_ectx : ectx → ectx → ectx := flip (++).
+
+  Definition fill (K : ectx) (e : expr) : expr := foldl (flip fill_item) e K.
+  Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
+  Proof. apply foldl_app. Qed.
+  Lemma fill_empty e : fill empty_ectx e = e.
+  Proof. done. Qed.
+  Lemma fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
+  Proof. unfold fill, comp_ectx; simpl. by rewrite foldl_app. Qed.
+  Global Instance fill_inj K : Inj (=) (=) (fill K).
+  Proof. induction K as [|Ki K IH]; unfold Inj; naive_solver. Qed.
+
+  Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
+  Proof.
+    induction K as [|Ki K IH] in e |-*; [ done |]. by intros ?%IH%fill_item_val.
+  Qed.
+  Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
+  Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
+
+End contexts.
+
+(** Contextual steps *)
+Inductive contextual_step : expr * heap → expr * heap → Prop :=
+  Ectx_step K e1 e2 σ1 σ2 e1' e2' :
+    e1 = fill K e1' → e2 = fill K e2' →
+    base_step (e1', σ1) (e2', σ2) → contextual_step (e1, σ1) (e2, σ2).
+
+
+Lemma base_contextual_step e1 e2 σ1 σ2 :
+  base_step (e1, σ1) (e2, σ2) → contextual_step (e1, σ1) (e2, σ2).
+Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
+
+Lemma fill_contextual_step K e1 e2 σ1 σ2 :
+  contextual_step (e1, σ1) (e2, σ2) → contextual_step (fill K e1, σ1) (fill K e2, σ2).
+Proof.
+  inversion 1; subst.
+  rewrite !fill_comp. by econstructor.
+Qed.
+
+(** *** closedness *)
+Fixpoint is_closed (X : list string) (e : expr) : bool :=
+  match e with
+  | Var x => bool_decide (x ∈ X)
+  | Lam x e => is_closed (x :b: X) e
+  | Unpack x e1 e2 => is_closed X e1 && is_closed (x :b: X) e2
+  | Lit _ => true
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | TApp e | TLam e | Pack e | Roll e | Unroll e | Load e | New e=> is_closed X e
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 => is_closed X e1 && is_closed X e2
+  |  If e0 e1 e2 | Case e0 e1 e2 =>
+   is_closed X e0 && is_closed X e1 && is_closed X e2
+  end.
+
+(** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *)
+Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e).
+#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
+Proof. unfold closed. apply _. Qed.
+#[export] Instance closed_dec X e : Decision (closed X e).
+Proof. unfold closed. apply _. Defined.
+
+(** closed expressions *)
+Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
+Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
+
+Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
+Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
+
+Lemma is_closed_subst X e x es :
+  is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).
+Proof.
+  intros ?.
+  induction e in X |-*; simpl; intros ?; destruct_and?; split_and?; simplify_option_eq;
+    try match goal with
+    | H : ¬(_ ∧ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
+    end; eauto using is_closed_weaken with set_solver.
+Qed.
+Lemma is_closed_do_subst' X e x es :
+  is_closed [] es → is_closed (x :b: X) e → is_closed X (subst' x es e).
+Proof. destruct x; eauto using is_closed_subst. Qed.
+
+Lemma closed_is_closed X e :
+  is_closed X e = true ↔ closed X e.
+Proof.
+  unfold closed. split.
+  - apply Is_true_eq_left.
+  - apply Is_true_eq_true.
+Qed.
+
+(** Substitution lemmas *)
+Lemma subst_is_closed X e x es : is_closed X e → x ∉ X → subst x es e = e.
+Proof.
+  induction e in X |-*; simpl; rewrite ?bool_decide_spec ?andb_True; intros ??;
+    repeat case_decide; simplify_eq; simpl; f_equal; intuition eauto with set_solver.
+Qed.
+
+Lemma subst_is_closed_nil e x es : is_closed [] e → subst x es e = e.
+Proof. intros. apply subst_is_closed with []; set_solver. Qed.
+Lemma subst'_is_closed_nil e x es : is_closed [] e → subst' x es e = e.
+Proof. intros. destruct x as [ | x]. { done. } by apply subst_is_closed_nil. Qed.
+
+(** ** More on the contextual semantics *)
+
+Definition base_reducible (e : expr) σ :=
+  ∃ e' σ', base_step (e, σ) (e', σ').
+Definition base_irreducible (e : expr) σ :=
+  ∀ e' σ', ¬base_step (e, σ) (e', σ').
+Definition base_stuck (e : expr) σ :=
+  to_val e = None ∧ base_irreducible e σ.
+
+(** Given a base redex [e1_redex] somewhere in a term, and another
+    decomposition of the same term into [fill K' e1'] such that [e1'] is not
+    a value, then the base redex context is [e1']'s context [K'] filled with
+    another context [K''].  In particular, this implies [e1 = fill K''
+    e1_redex] by [fill_inj], i.e., [e1]' contains the base redex.)
+ *)
+Lemma step_by_val K' K_redex e1' e1_redex e2 σ1 σ2 :
+    fill K' e1' = fill K_redex e1_redex →
+    to_val e1' = None →
+    base_step (e1_redex, σ1) (e2, σ2) →
+    ∃ K'', K_redex = comp_ectx K' K''.
+Proof.
+  rename K' into K. rename K_redex into K'.
+  rename e1' into e1. rename e1_redex into e1'.
+  intros Hfill Hred Hstep; revert K' Hfill.
+  induction K as [|Ki K IH] using rev_ind; simpl; intros K' Hfill; eauto using app_nil_r.
+  destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
+  { rewrite fill_app in Hstep. apply base_ectxi_step_val in Hstep.
+    apply fill_val in Hstep. by apply not_eq_None_Some in Hstep. }
+  rewrite !fill_app in Hfill; simpl in Hfill.
+  assert (Ki = Ki') as ->.
+  { eapply fill_item_no_val_inj, Hfill.
+    - by apply fill_not_val.
+    - apply fill_not_val. eauto using val_base_stuck.
+  }
+  simplify_eq. destruct (IH K') as [K'' ->]; auto.
+  exists K''. unfold comp_ectx; simpl. rewrite assoc; done.
+Qed.
+
+(** If [fill K e] takes a base step, then either [e] is a value or [K] is
+    the empty evaluation context. In other words, if [e] is not a value
+    wrapping it in a context does not add new base redex positions. *)
+Lemma base_ectx_step_val K e e2 σ1 σ2 :
+  base_step (fill K e, σ1) (e2, σ2) → is_Some (to_val e) ∨ K = empty_ectx.
+Proof.
+  destruct K as [|Ki K _] using rev_ind; simpl; [by auto|].
+  rewrite fill_app; simpl.
+  intros ?%base_ectxi_step_val; eauto using fill_val.
+Qed.
+
+(** If a [contextual_step] preserving a surrounding context [K] happens,
+   the reduction happens entirely below the context. *)
+Lemma contextual_step_ectx_inv K e e' σ1 σ2 :
+  to_val e = None →
+  contextual_step (fill K e, σ1) (fill K e', σ2) →
+  contextual_step (e, σ1) (e', σ2).
+Proof.
+  intros ? Hcontextual.
+  inversion Hcontextual as [??????? Heq1 Heq2 ?]; subst.
+  eapply step_by_val in H as (K'' & Heq); [ | done | done].
+  subst K0.
+  rewrite <-fill_comp in Heq1. rewrite <-fill_comp in Heq2.
+  apply fill_inj in Heq1. apply fill_inj in Heq2. subst.
+  econstructor; done.
+Qed.
+
+Lemma contextual_ectx_step_case K e e' σ1 σ2 :
+  contextual_step (fill K e, σ1) (e', σ2) →
+  (∃ e'', e' = fill K e'' ∧ contextual_step (e, σ1) (e'', σ2)) ∨ is_val e.
+Proof.
+  destruct (to_val e) as [ v | ] eqn:Hv.
+  { intros _. right. apply is_val_spec. eauto. }
+  intros Hcontextual. left.
+  inversion Hcontextual as [K' ? ? ? ? e1' e2' Heq1 Heq2 Hstep]; subst.
+  eapply step_by_val in Heq1 as (K'' & ->); [ | done | done].
+  rewrite <-fill_comp.
+  eexists _. split; [done | ].
+  rewrite <-fill_comp in Hcontextual.
+  apply contextual_step_ectx_inv in Hcontextual; done.
+Qed.
+
+Lemma base_reducible_contextual_step_ectx K e1 e2 σ1 σ2 :
+  base_reducible e1 σ1 →
+  contextual_step (fill K e1, σ1) (e2, σ2) →
+  ∃ e2', e2 = fill K e2' ∧ base_step (e1, σ1) (e2', σ2).
+Proof.
+  intros (e2''&σ2'' & HhstepK) Hctx.
+  inversion Hctx as [K' ???? e1' e2' HKe1 -> Hstep].
+  edestruct (step_by_val K) as [K'' ?];
+    eauto using val_base_stuck; simplify_eq/=.
+  rewrite <-fill_comp in HKe1; simplify_eq.
+  exists (fill K'' e2'). rewrite fill_comp; split; [done | ].
+  apply base_ectx_step_val in HhstepK as [[v ?]|?]; simplify_eq.
+  { apply val_base_stuck in Hstep; simplify_eq. }
+  by rewrite !fill_empty.
+Qed.
+
+Lemma base_reducible_contextual_step e1 e2 σ1 σ2 :
+  base_reducible e1 σ1 →
+  contextual_step (e1, σ1) (e2, σ2) →
+  base_step (e1, σ1) (e2, σ2).
+Proof.
+  intros.
+  edestruct (base_reducible_contextual_step_ectx empty_ectx) as (?&?&?);
+    rewrite ?fill_empty; eauto.
+  by simplify_eq; rewrite fill_empty.
+Qed.
+
+(** *** Reducibility *)
+Definition reducible (e : expr) σ :=
+    ∃ e' σ', contextual_step (e, σ) (e', σ').
+Definition irreducible (e : expr) σ :=
+  ∀ e' σ', ¬contextual_step (e, σ) (e', σ').
+Definition stuck (e : expr) σ :=
+  to_val e = None ∧ irreducible e σ.
+Definition not_stuck (e : expr) σ :=
+  is_Some (to_val e) ∨ reducible e σ.
+
+Lemma base_step_not_stuck e e' σ σ' : base_step (e, σ) (e', σ') → not_stuck e σ.
+Proof. unfold not_stuck, reducible; simpl. eauto 10 using base_contextual_step. Qed.
+
+Lemma val_stuck e e' σ σ' : contextual_step (e, σ) (e', σ') → to_val e = None.
+Proof.
+  inversion 1 as [??????? -> -> ?%val_base_stuck].
+  apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
+Qed.
+Lemma not_reducible e σ : ¬reducible e σ ↔ irreducible e σ.
+Proof. unfold reducible, irreducible. naive_solver. Qed.
+Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
+Proof. intros (?&?&?). eauto using val_stuck. Qed.
+Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ.
+Proof. intros [??] ?? ?%val_stuck. by destruct (to_val e). Qed.
+
+Lemma irreducible_fill K e σ :
+  irreducible (fill K e) σ → irreducible e σ.
+Proof.
+  intros Hirred e' σ' Hstep.
+  eapply Hirred. by apply fill_contextual_step.
+Qed.
+
+Lemma base_reducible_reducible e σ :
+  base_reducible e σ → reducible e σ.
+Proof. intros (e' & σ' & Hhead). exists e', σ'. by apply base_contextual_step. Qed.
+
+
+(* we derive a few lemmas about contextual steps *)
+Lemma contextual_step_app_l e1 e1' e2 σ1 σ2 :
+  is_val e2 →
+  contextual_step (e1, σ1) (e1', σ2) →
+  contextual_step (App e1 e2, σ1) (App e1' e2, σ2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step [AppLCtx _]).
+Qed.
+
+Lemma contextual_step_app_r e1 e2 e2' σ1 σ2 :
+  contextual_step (e2, σ1) (e2', σ2) →
+  contextual_step (App e1 e2, σ1) (App e1 e2', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [AppRCtx e1]).
+Qed.
+
+Lemma contextual_step_tapp e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (TApp e, σ1) (TApp e', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [TAppCtx]).
+Qed.
+
+Lemma contextual_step_pack e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (Pack e, σ1) (Pack e', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [PackCtx]).
+Qed.
+
+Lemma contextual_step_unpack x e e' e2 σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (Unpack x e e2, σ1) (Unpack x e' e2, σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [UnpackCtx x e2]).
+Qed.
+
+Lemma contextual_step_unop op e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (UnOp op e, σ1) (UnOp op e', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [UnOpCtx op]).
+Qed.
+
+Lemma contextual_step_binop_l op e1 e1' e2 σ1 σ2 :
+  is_val e2 →
+  contextual_step (e1, σ1) (e1', σ2) →
+  contextual_step (BinOp op e1 e2, σ1) (BinOp op e1' e2, σ2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step [BinOpLCtx op v]).
+Qed.
+
+Lemma contextual_step_binop_r op e1 e2 e2' σ1 σ2 :
+  contextual_step (e2, σ1) (e2', σ2) →
+  contextual_step (BinOp op e1 e2, σ1) (BinOp op e1 e2', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [BinOpRCtx op e1]).
+Qed.
+
+Lemma contextual_step_if e e' e1 e2 σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (If e e1 e2, σ1) (If e' e1 e2, σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [IfCtx e1 e2]).
+Qed.
+
+Lemma contextual_step_pair_l e1 e1' e2 σ1 σ2 :
+  is_val e2 →
+  contextual_step (e1, σ1) (e1', σ2) →
+  contextual_step (Pair e1 e2, σ1) (Pair e1' e2, σ2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step [PairLCtx v]).
+Qed.
+
+Lemma contextual_step_pair_r e1 e2 e2' σ1 σ2 :
+  contextual_step (e2, σ1) (e2', σ2) →
+  contextual_step (Pair e1 e2, σ1) (Pair e1 e2', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [PairRCtx e1]).
+Qed.
+
+
+Lemma contextual_step_fst e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (Fst e, σ1) (Fst e', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [FstCtx]).
+Qed.
+
+Lemma contextual_step_snd e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (Snd e, σ1) (Snd e', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [SndCtx]).
+Qed.
+
+Lemma contextual_step_injl e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (InjL e, σ1) (InjL e', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [InjLCtx]).
+Qed.
+
+Lemma contextual_step_injr e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (InjR e, σ1) (InjR e', σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [InjRCtx]).
+Qed.
+
+Lemma contextual_step_case e e' e1 e2 σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (Case e e1 e2, σ1) (Case e' e1 e2, σ2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [CaseCtx e1 e2]).
+Qed.
+
+Lemma contextual_step_roll e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (Roll e, σ1) (Roll e', σ2).
+Proof. by apply (fill_contextual_step [RollCtx]). Qed.
+
+Lemma contextual_step_unroll e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (Unroll e, σ1) (Unroll e', σ2).
+Proof. by apply (fill_contextual_step [UnrollCtx]). Qed.
+
+Lemma contextual_step_new e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (New e, σ1) (New e', σ2).
+Proof. by apply (fill_contextual_step [NewCtx]). Qed.
+
+Lemma contextual_step_load e e' σ1 σ2 :
+  contextual_step (e, σ1) (e', σ2) →
+  contextual_step (Load e, σ1) (Load e', σ2).
+Proof. by apply (fill_contextual_step [LoadCtx]). Qed.
+
+Lemma contextual_step_store_r e1 e2 e2' σ1 σ2 :
+  contextual_step (e2, σ1) (e2', σ2) →
+  contextual_step (Store e1 e2, σ1) (Store e1 e2', σ2).
+Proof. by apply (fill_contextual_step [StoreRCtx _]). Qed.
+
+Lemma contextual_step_store_l e1 e1' e2 σ1 σ2 :
+  is_val e2 →
+  contextual_step (e1, σ1) (e1', σ2) →
+  contextual_step (Store e1 e2, σ1) (Store e1' e2, σ2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step [StoreLCtx _]).
+Qed.
+
+
+#[export]
+Hint Resolve
+  contextual_step_app_l contextual_step_app_r contextual_step_binop_l contextual_step_binop_r
+  contextual_step_case contextual_step_fst contextual_step_if contextual_step_injl contextual_step_injr
+  contextual_step_pack contextual_step_pair_l contextual_step_pair_r contextual_step_snd contextual_step_tapp
+  contextual_step_tapp contextual_step_unop contextual_step_unpack contextual_step_roll contextual_step_unroll
+  contextual_step_new contextual_step_load contextual_step_store_r contextual_step_store_l : core.
diff --git a/theories/type_systems/systemf_mu_state/locations.v b/theories/type_systems/systemf_mu_state/locations.v
new file mode 100644
index 0000000..f3dda15
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/locations.v
@@ -0,0 +1,46 @@
+From stdpp Require Import countable numbers gmap.
+
+Record loc := Loc { loc_car : Z }.
+
+Add Printing Constructor loc.
+
+Global Instance loc_eq_decision : EqDecision loc.
+Proof. solve_decision. Defined.
+
+Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
+
+Global Instance loc_countable : Countable loc.
+Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
+
+Global Program Instance loc_infinite : Infinite loc :=
+  inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
+Next Obligation. done. Qed.
+
+Definition loc_add (l : loc) (off : Z) : loc :=
+  {| loc_car := loc_car l + off|}.
+
+Notation "l +ₗ off" :=
+  (loc_add l off) (at level 50, left associativity) : stdpp_scope.
+
+Lemma loc_add_assoc l i j : l +ₗ i +ₗ j = l +ₗ (i + j).
+Proof. destruct l; unfold loc_add; simpl; f_equal; lia. Qed.
+
+Lemma loc_add_0 l : l +ₗ 0 = l.
+Proof. destruct l; unfold loc_add; simpl; f_equal; lia. Qed.
+
+Global Instance loc_add_inj l : Inj eq eq (loc_add l).
+Proof. destruct l; unfold Inj, loc_add; simpl; intros; simplify_eq; lia. Qed.
+
+Definition fresh_locs (ls : gset loc) : loc :=
+  {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z ls |}.
+
+Lemma fresh_locs_fresh ls i :
+  (0 ≤ i)%Z → fresh_locs ls +ₗ i ∉ ls.
+Proof.
+  intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh_locs ls) + i)%Z.
+  { intros help Hf%help. simpl in *. lia. }
+  apply (set_fold_ind_L (λ r ls, ∀ l, l ∈ ls → (loc_car l < r + i)%Z));
+    set_solver by eauto with lia.
+Qed.
+
+Global Opaque fresh_locs.
diff --git a/theories/type_systems/systemf_mu_state/logrel.v b/theories/type_systems/systemf_mu_state/logrel.v
new file mode 100644
index 0000000..52e0286
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/logrel.v
@@ -0,0 +1,1738 @@
+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. *)
+  (* TODO: exercise *)
+Admitted.
+
+
+
+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/notation.v b/theories/type_systems/systemf_mu_state/notation.v
new file mode 100644
index 0000000..e4d1cd0
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/notation.v
@@ -0,0 +1,113 @@
+From semantics.ts.systemf_mu_state Require Export lang.
+Set Default Proof Using "Type".
+
+
+(** Coercions to make programs easier to type. *)
+Coercion of_val : val >-> expr.
+Coercion LitInt : Z >-> base_lit.
+Coercion LitBool : bool >-> base_lit.
+Coercion LitLoc : loc >-> base_lit.
+
+Coercion App : expr >-> Funclass.
+Coercion Var : string >-> expr.
+
+(** Define some derived forms. *)
+Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
+Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
+
+(* No scope for the values, does not conflict and scope is often not inferred
+properly. *)
+Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
+Notation "# l" := (Lit l%Z%E%stdpp) (at level 8, format "# l") : expr_scope.
+
+(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
+    first. *)
+Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
+Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
+
+Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
+  (Match e0 x1%binder e1 x2%binder e2)
+  (e0, x1, e1, x2, e2 at level 200,
+   format "'[hv' 'match:'  e0  'with'  '/  ' '[' 'InjL'  x1  =>  '/  ' e1 ']'  '/' '[' |  'InjR'  x2  =>  '/  ' e2 ']'  '/' 'end' ']'") : expr_scope.
+Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
+  (Match e0 x2%binder e2 x1%binder e1)
+  (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
+
+Notation "()" := LitUnit : val_scope.
+
+Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.
+Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope.
+Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope.
+Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope.
+Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope.
+Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) : expr_scope.
+
+(*Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.*)
+
+Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
+  (at level 200, e1, e2, e3 at level 200) : expr_scope.
+
+Notation "λ: x , e" := (Lam x%binder e%E)
+  (at level 200, x at level 1, e at level 200,
+   format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
+Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
+  (at level 200, x, y, z at level 1, e at level 200,
+   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.
+
+Notation "λ: x , e" := (LamV x%binder e%E)
+  (at level 200, x at level 1, e at level 200,
+   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
+Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
+  (at level 200, x, y, z at level 1, e at level 200,
+   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
+
+Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
+  (at level 200, x at level 1, e1, e2 at level 200,
+   format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
+Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
+  (at level 100, e2 at level 200,
+   format "'[' '[hv' '[' e1 ']' ;;  ']' '/' e2 ']'") : expr_scope.
+
+
+Notation "'Λ' , e" := (TLam e%E)
+  (at level 200, e at level 200,
+    format "'[' 'Λ' , '/  ' e ']'") : expr_scope.
+Notation "'Λ' , e" := (TLamV e%E)
+  (at level 200, e at level 200,
+    format "'[' 'Λ' , '/  ' e ']'") : val_scope.
+
+(* the [e] always needs to be paranthesized, due to the level
+   (chosen to make this cooperate with the [App] coercion) *)
+Notation "e '<>'" := (TApp e%E)
+  (at level 10) : expr_scope.
+(*Check ((Λ, #4) <>)%E.*)
+(*Check (((λ: "x", "x") #5) <>)%E.*)
+
+Notation "'pack' e" := (Pack e%E)
+  (at level 200, e at level 200) : expr_scope.
+Notation "'pack' v" := (PackV v%V)
+  (at level 200, v at level 200) : val_scope.
+Notation "'unpack'  e1  'as'  x  'in'  e2" := (Unpack x%binder e1%E e2%E)
+  (at level 200, e1, e2 at level 200, x at level 1) : expr_scope.
+
+Notation "'roll'  e" := (Roll e%E)
+  (at level 200, e at level 200) : expr_scope.
+Notation "'roll'  v" := (RollV v%E)
+  (at level 200, v at level 200) : val_scope.
+Notation "'unroll'  e" := (Unroll e%E)
+  (at level 200, e at level 200) : expr_scope.
+
+Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
+Notation "'new' e" := (New e%E) (at level 10) : expr_scope.
+Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
+
+
+Definition assert (e : expr) : expr :=
+  if: e then #LitUnit else (#0 #0).
+Definition Or (e1 e2 : expr) : expr :=
+  if: e1 then #true else e2.
+Definition And (e1 e2 : expr) : expr :=
+  if: e1 then e2 else #false.
+Notation "e1 '||' e2" := (Or e1 e2) : expr_scope.
+Notation "e1 '&&' e2" := (And e1 e2) : expr_scope.
diff --git a/theories/type_systems/systemf_mu_state/parallel_subst.v b/theories/type_systems/systemf_mu_state/parallel_subst.v
new file mode 100644
index 0000000..2d177d8
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/parallel_subst.v
@@ -0,0 +1,279 @@
+From stdpp Require Import prelude.
+From iris Require Import prelude.
+From semantics.lib Require Import facts.
+From semantics.ts.systemf_mu_state Require Import lang.
+From semantics.lib Require Import maps.
+
+Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
+  match e with
+  | Lit l => Lit l
+  | Var y => match xs !! y with Some es => es | _ =>  Var y end
+  | App e1 e2 => App (subst_map xs e1) (subst_map xs e2)
+  | Lam x e => Lam x (subst_map (binder_delete x xs) e)
+  | UnOp op e => UnOp op (subst_map xs e)
+  | BinOp op e1 e2 => BinOp op (subst_map xs e1) (subst_map xs e2)
+  | If e0 e1 e2 => If (subst_map xs e0) (subst_map xs e1) (subst_map xs e2)
+  | TApp e => TApp (subst_map xs e)
+  | TLam e => TLam (subst_map xs e)
+  | Pack e => Pack (subst_map xs e)
+  | Unpack x e1 e2 => Unpack x (subst_map xs e1) (subst_map (binder_delete x xs) e2)
+  | Pair e1 e2 => Pair (subst_map xs e1) (subst_map xs e2)
+  | Fst e => Fst (subst_map xs e)
+  | Snd e => Snd (subst_map xs e)
+  | InjL e => InjL (subst_map xs e)
+  | InjR e => InjR (subst_map xs e)
+  | Case e e1 e2 => Case (subst_map xs e) (subst_map xs e1) (subst_map xs e2)
+  | Roll e => Roll (subst_map xs e)
+  | Unroll e => Unroll (subst_map xs e)
+  | Load e => Load (subst_map xs e)
+  | Store e1 e2 => Store (subst_map xs e1) (subst_map xs e2)
+  | New e => New (subst_map xs e)
+  end.
+
+Lemma subst_map_empty e :
+  subst_map ∅ e = e.
+Proof.
+  induction e; simpl; f_equal; eauto.
+  all: destruct x; simpl; [done | by rewrite !delete_empty..].
+Qed.
+
+Lemma subst_map_is_closed X e xs :
+  is_closed X e →
+  (∀ x : string, x ∈ dom xs → x ∉ X) →
+  subst_map xs e = e.
+Proof.
+  intros Hclosed Hd.
+  induction e in xs, X, Hd, Hclosed |-*; simpl in *;try done.
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  { (* Var *)
+    apply bool_decide_spec in Hclosed.
+    assert (xs !! x = None) as ->; last done.
+    destruct (xs !! x) as [s | ] eqn:Helem; last done.
+    exfalso; eapply Hd; last apply Hclosed.
+    apply elem_of_dom; eauto.
+  }
+  { (* lambdas *)
+    erewrite IHe; [done | done |].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  8: { (* Unpack *)
+    erewrite IHe1; [ | done | done].
+    erewrite IHe2; [ done | done | ].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+       | H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H
+       end; done.
+Qed.
+
+Lemma subst_map_subst map x (e e' : expr) :
+  is_closed [] e' →
+  subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e.
+Proof.
+  intros He'.
+  revert x map; induction e; intros xx map; simpl;
+  try (f_equal; eauto).
+  - case_decide.
+    + simplify_eq/=. rewrite lookup_insert.
+      rewrite (subst_map_is_closed []); [done | apply He' | ].
+      intros ? ?. apply not_elem_of_nil.
+    + rewrite lookup_insert_ne; done.
+  - destruct x; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+  - destruct x; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+Qed.
+
+Definition subst_is_closed (X : list string) (map : gmap string expr) :=
+  ∀ x e, map !! x = Some e → closed X e.
+Lemma subst_is_closed_subseteq X map1 map2 :
+  map1 ⊆ map2 → subst_is_closed X map2 → subst_is_closed X map1.
+Proof.
+  intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done.
+Qed.
+
+Lemma subst_subst_map x es map e :
+  subst_is_closed [] map →
+  subst x es (subst_map (delete x map) e) =
+  subst_map (<[x:=es]>map) e.
+Proof.
+  revert map es x; induction e; intros map v0 xx Hclosed; simpl;
+  try (f_equal; eauto).
+  - destruct (decide (xx=x)) as [->|Hne].
+    + rewrite lookup_delete // lookup_insert //. simpl.
+      rewrite decide_True //.
+    + rewrite lookup_delete_ne // lookup_insert_ne //.
+      destruct (_ !! x) as [rr|] eqn:Helem.
+      * apply Hclosed in Helem.
+        by apply subst_is_closed_nil.
+      * simpl. rewrite decide_False //.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe.
+      eapply subst_is_closed_subseteq; last done.
+      apply map_delete_subseteq.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe2.
+      eapply subst_is_closed_subseteq; last done.
+      apply map_delete_subseteq.
+Qed.
+
+Lemma subst'_subst_map b (es : expr) map e :
+  subst_is_closed [] map →
+  subst' b es (subst_map (binder_delete b map) e) =
+  subst_map (binder_insert b es map) e.
+Proof.
+  destruct b; first done.
+  apply subst_subst_map.
+Qed.
+
+Lemma closed_subst_weaken e map X Y :
+  subst_is_closed [] map →
+  (∀ x, x ∈ X → x ∉ dom map → x ∈ Y) →
+  closed X e →
+  closed Y (subst_map map e).
+Proof.
+  induction e in X, Y, map |-*; rewrite /closed; simpl; intros Hmclosed Hsub Hcl; first done.
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  { (* vars *)
+    destruct (map !! x) as [es | ] eqn:Heq.
+    + apply is_closed_weaken_nil. by eapply Hmclosed.
+    + apply bool_decide_pack. apply Hsub; first by eapply bool_decide_unpack.
+      by apply not_elem_of_dom.
+  }
+  { (* lambdas *)
+    eapply IHe; last done.
+    + eapply subst_is_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  8: { (* unpack *)
+    apply andb_True; split; first naive_solver.
+    eapply IHe2; last done.
+    + eapply subst_is_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+         | |- Is_true (_ && _) => apply andb_True; split
+              end.
+  all: naive_solver.
+Qed.
+
+Lemma subst_is_closed_weaken X1 X2 θ :
+  subst_is_closed X1 θ →
+  X1 ⊆ X2 →
+  subst_is_closed X2 θ.
+Proof.
+  intros Hcl Hincl x e Hlook.
+  eapply is_closed_weaken; last done.
+  by eapply Hcl.
+Qed.
+
+Lemma subst_is_closed_weaken_nil X θ :
+  subst_is_closed [] θ →
+  subst_is_closed X θ.
+Proof.
+  intros; eapply subst_is_closed_weaken; first done.
+  apply list_subseteq_nil.
+Qed.
+
+Lemma subst_is_closed_insert X e f θ :
+  is_closed X e →
+  subst_is_closed X (delete f θ) →
+  subst_is_closed X (<[f := e]> θ).
+Proof.
+  intros Hcl Hcl' x e'.
+  destruct (decide (x = f)) as [<- | ?].
+  - rewrite lookup_insert. intros [= <-]. done.
+  - rewrite lookup_insert_ne; last done.
+    intros Hlook. eapply Hcl'.
+    rewrite lookup_delete_ne; done.
+Qed.
+
+(* NOTE: this is a simplified version of the tactic in tactics.v which
+  suffice for this proof *)
+Ltac simplify_closed :=
+  repeat match goal with
+  | |- closed _ _ => unfold closed; simpl
+  | |- Is_true (_ && _)  => simpl; rewrite !andb_True; split_and!
+  | H : closed _ _ |- _ => unfold closed in H; simpl in H
+  | H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H
+  | H : _ ∧ _ |- _ => destruct H
+  end.
+
+Lemma is_closed_subst_map X θ e :
+  subst_is_closed X θ →
+  closed (X ++ elements (dom θ)) e →
+  closed X (subst_map θ e).
+Proof.
+  induction e in X, θ |-*; eauto.
+  all: try solve [intros; simplify_closed; naive_solver].
+  - unfold subst_map.
+    destruct (θ !! x) eqn:Heq.
+    + intros Hcl _. eapply Hcl; done.
+    + intros _ Hcl.
+      apply closed_is_closed in Hcl.
+      apply bool_decide_eq_true in Hcl.
+      apply elem_of_app in Hcl.
+      destruct Hcl as [ | H].
+      * apply closed_is_closed. by apply bool_decide_eq_true.
+      * apply elem_of_elements in H.
+        by apply not_elem_of_dom in Heq.
+  - intros. simplify_closed.
+    eapply IHe.
+    + destruct x as [ | x]; simpl; first done.
+      intros y e'. rewrite lookup_delete_Some. intros (? & Hlook%H).
+      eapply is_closed_weaken; first done.
+      by apply list_subseteq_cons_r.
+    + eapply is_closed_weaken; first done.
+      simpl. destruct x as [ | x]; first done; simpl.
+      apply list_subseteq_cons_l.
+      apply stdpp.sets.elem_of_subseteq.
+      intros y; simpl. rewrite elem_of_cons !elem_of_app.
+      intros [ | Helem]; first naive_solver.
+      destruct (decide (x = y)) as [<- | Hneq]; first naive_solver.
+      right. right. apply elem_of_elements. rewrite dom_delete elem_of_difference elem_of_singleton.
+      apply elem_of_elements in Helem; done.
+  - intros. simplify_closed. { naive_solver. }
+    (* same proof as for lambda *)
+    eapply IHe2.
+    + destruct x as [ | x]; simpl; first done.
+      intros y e'. rewrite lookup_delete_Some. intros (? & Hlook%H).
+      eapply is_closed_weaken; first done.
+      by apply list_subseteq_cons_r.
+    + eapply is_closed_weaken; first done.
+      simpl. destruct x as [ | x]; first done; simpl.
+      apply list_subseteq_cons_l.
+      apply stdpp.sets.elem_of_subseteq.
+      intros y; simpl. rewrite elem_of_cons !elem_of_app.
+      intros [ | Helem]; first naive_solver.
+      destruct (decide (x = y)) as [<- | Hneq]; first naive_solver.
+      right. right. apply elem_of_elements. rewrite dom_delete elem_of_difference elem_of_singleton.
+      apply elem_of_elements in Helem; done.
+Qed.
diff --git a/theories/type_systems/systemf_mu_state/tactics.v b/theories/type_systems/systemf_mu_state/tactics.v
new file mode 100644
index 0000000..a38ae75
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/tactics.v
@@ -0,0 +1,91 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Export facts maps sets.
+From semantics.ts.systemf_mu_state Require Export lang notation parallel_subst types.
+
+Ltac map_solver :=
+  repeat match goal with
+         | |-  (⤉ _) !! _ = Some _ =>
+             rewrite fmap_insert
+         | |- <[ ?p := _ ]> _ !! ?p = Some _ =>
+             apply lookup_insert
+         | |- <[ _ := _ ]> _ !! _ = Some _ =>
+             rewrite lookup_insert_ne; [ | congruence]
+         end.
+
+Ltac solve_typing_step := idtac.
+Ltac solve_typing :=
+  intros;
+  repeat (asimpl; solve_typing_step).
+Ltac solve_typing_fast := 
+  intros;
+  repeat (solve_typing_step).
+Ltac solve_typing_step ::=
+  match goal with
+  | |- TY _; _ ; _ ⊢ ?e : ?A => first [eassumption | econstructor]
+  (* heuristic to solve tapp goals where we need to pick the right type for the substitution *)
+  | |- TY _ ; _ ; _ ⊢ ?e <> : ?A => eapply typed_tapp'; [solve_typing | | asimpl; reflexivity]
+  | |- TY _ ; _ ; _ ⊢ Unroll ?e : ?A => eapply typed_unroll'; [solve_typing | asimpl; reflexivity]
+  | |- bin_op_typed _ _ _ _ => econstructor
+  | |- un_op_typed _ _ _ _ => econstructor
+  | |- type_wf _ ?e => assert_fails (is_evar e); eassumption
+  | |- type_wf _ ?e => assert_fails (is_evar e); econstructor
+  | |- type_wf _ (subst _ ?A) => eapply type_wf_subst; [ | intros; simpl]
+  | |- type_wf _ ?e => assert_fails (is_evar e); eapply type_wf_mono; [eassumption | lia]
+  (* conditions spawned by the tyvar case of [type_wf] *)
+  | |- _ < _ => simpl; lia
+  (* conditions spawned by the variable case *)
+  | |- _ !! _ = Some _ => map_solver
+  end.
+
+Tactic Notation "unify_type" uconstr(A) :=
+  match goal with
+  | |- TY ?Σ; ?n; ?Γ ⊢ ?e : ?B => unify A B
+  end.
+Tactic Notation "replace_type" uconstr(A) :=
+  match goal with
+  | |- TY ?Σ; ?n; ?Γ ⊢ ?e : ?B => replace B%ty with A%ty; cycle -1; first try by asimpl
+  end.
+
+
+Ltac simplify_list_elem :=
+  simpl;
+  repeat match goal with
+         | |- ?x ∈ ?y :: ?l => apply elem_of_cons; first [left; reflexivity | right]
+         | |- _ ∉ [] => apply not_elem_of_nil
+         | |- _ ∉ _ :: _ => apply not_elem_of_cons; split
+  end; try fast_done.
+Ltac simplify_list_subseteq :=
+  simpl;
+  repeat match goal with
+         | |- ?x :: _ ⊆ ?x :: _ => apply list_subseteq_cons_l
+         | |- ?x :: _ ⊆ _ => apply list_subseteq_cons_elem; first solve [simplify_list_elem]
+         | |- elements _ ⊆ elements _ => apply elements_subseteq; set_solver
+         | |- [] ⊆ _ => apply list_subseteq_nil
+         | |- ?x :b: _ ⊆ ?x :b: _ => apply list_subseteq_cons_binder
+         (* NOTE: this might make the goal unprovable *)
+         (*| |- elements _ ⊆ _ :: _ => apply list_subseteq_cons_r*)
+         end;
+  try fast_done.
+
+(* Try to solve [is_closed] goals using a number of heuristics (that shouldn't make the goal unprovable) *)
+Ltac simplify_closed :=
+  simpl; intros;
+  repeat match goal with
+  | |- closed _ _ => unfold closed; simpl
+  | |- Is_true (is_closed [] _) => first [assumption | done]
+  | |- Is_true (is_closed _ (lang.subst _ _ _)) => rewrite subst_is_closed_nil; last solve[simplify_closed]
+  | |- Is_true (is_closed ?X ?v) => assert_fails (is_evar X); eapply is_closed_weaken
+  | |- Is_true (is_closed _ _) => eassumption
+  | |- Is_true (_ && true) => rewrite andb_true_r
+  | |- Is_true (true && _) => rewrite andb_true_l
+  | |- Is_true (?a && ?a) => rewrite andb_diag
+  | |- Is_true (_ && _)  => simpl; rewrite !andb_True; split_and!
+  | |- _ ⊆ ?A => match type of A with | list _ => simplify_list_subseteq end
+  | |- _ ∈ ?A => match type of A with | list _ => simplify_list_elem end
+  | |- _ ≠ _ => congruence
+  | H : closed _ _ |- _ => unfold closed in H; simpl in H
+  | H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H
+  | H : _ ∧ _ |- _ => destruct H
+  | |- Is_true (bool_decide (_ ∈ _)) => apply bool_decide_pack; set_solver
+  end; try fast_done.
diff --git a/theories/type_systems/systemf_mu_state/types.v b/theories/type_systems/systemf_mu_state/types.v
new file mode 100644
index 0000000..0b020ed
--- /dev/null
+++ b/theories/type_systems/systemf_mu_state/types.v
@@ -0,0 +1,1326 @@
+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 *)
+    (* TODO: exercise *)
+    admit.
+  - (* load *)
+    (* TODO: exercise *)
+    admit.
+  - (* store *)
+    (* TODO: exercise *)
+    admit.
+Admitted.
+
+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.