Initialize repository

1 files changed, 2690 insertions, 0 deletions

diff --git a/theories/nix/interp_proofs.v b/theories/nix/interp_proofs.v
new file mode 100644
index 0000000..5780e48
--- /dev/null
+++ b/theories/nix/interp_proofs.v
@@ -0,0 +1,2690 @@
+From Coq Require Import Ascii.
+From mininix Require Export nix.interp.
+From stdpp Require Import options.
+
+Lemma force_deep_S n :
+  force_deep (S n) = force_deep1 (force_deep n) (interp_thunk n).
+Proof. done. Qed.
+Lemma interp_S n :
+  interp (S n) = interp1 (force_deep n) (interp n) (interp_thunk n) (interp_app n).
+Proof. done. Qed.
+Lemma interp_thunk_S n :
+  interp_thunk (S n) = interp_thunk1 (interp n) (interp_thunk n).
+Proof. done. Qed.
+Lemma interp_app_S n :
+  interp_app (S n) = interp_app1 (interp n) (interp_thunk n) (interp_app n).
+Proof. done. Qed.
+
+Lemma interp_shallow' m E e : interp' m SHALLOW E e = interp m E e.
+Proof. rewrite /interp'. by destruct (interp _ _ _) as [[]|]. Qed.
+
+Lemma interp_lit n E bl (Hbl : base_lit_ok bl) :
+  interp (S n) E (ELit bl) = mret (VLit bl Hbl).
+Proof.
+  rewrite interp_S /=. case_guard; simpl; [|done].
+  do 2 f_equal. apply (proof_irrel _).
+Qed.
+
+(** Induction *)
+Fixpoint val_size (v : val) : nat :=
+  match v with
+  | VLit _ _ => 1
+  | VClo _ E _ | VCloMatch E _ _ _ => S (map_sum_with (thunk_size ∘ snd) E)
+  | VList ts => S (sum_list_with thunk_size ts)
+  | VAttr ts => S (map_sum_with thunk_size ts)
+  end
+with thunk_size (t : thunk) : nat :=
+  match t with
+  | Forced v => S (val_size v)
+  | Thunk E _ => S (map_sum_with (thunk_size ∘ snd) E)
+  | Indirect _ E tαs => S (map_sum_with (thunk_size ∘ snd) E +
+      map_sum_with (from_sum (λ _, 1) thunk_size) tαs)
+  end.
+Notation env_size := (map_sum_with (thunk_size ∘ snd)).
+
+Definition from_thunk {A} (f : val → A) (g : env → expr → A)
+    (h : string → env → gmap string tattr → A) (t : thunk) : A :=
+  match t with
+  | Forced v => f v
+  | Thunk E e => g E e
+  | Indirect x E tαs => h x E tαs
+  end.
+
+Lemma env_val_ind (P : env → Prop) (Q : val → Prop) :
+  (∀ E,
+    map_Forall (λ _, from_thunk Q (λ E _, P E) (λ _ E _, P E) ∘ snd) E → P E) →
+  (∀ b Hbl, Q (VLit b Hbl)) →
+  (∀ x E e, P E → Q (VClo x E e)) →
+  (∀ E ms strict e, P E → Q (VCloMatch E ms strict e)) →
+  (∀ ts, Forall (from_thunk Q (λ E _, P E) (λ _ E _, P E)) ts → Q (VList ts)) →
+  (∀ ts, map_Forall (λ _, from_thunk Q (λ E _, P E) (λ _ E _, P E)) ts → Q (VAttr ts)) →
+  (∀ E, P E) ∧ (∀ v, Q v).
+Proof.
+  intros Penv Qlit Qclo Qmatch Qlist Qattr.
+  cut (∀ n, (∀ E, env_size E < n → P E) ∧ (∀ v, val_size v < n → Q v)).
+  { intros Hhelp; split.
+    - intros E. apply (Hhelp (S (env_size E))); lia.
+    - intros v. apply (Hhelp (S (val_size v))); lia. }
+  intros n. induction n as [|n IH]; [by auto with lia|]. split.
+  - intros E ?. apply Penv, map_Forall_lookup=> y [k ei] Hy.
+    apply (map_sum_with_lookup_le (thunk_size ∘ snd)) in Hy; simpl in *.
+    destruct ei as [v|E' e'|x E' tαs]; simplify_eq/=; try apply IH; eauto with lia.
+  - intros [] ?; simpl in *.
+    + apply Qlit.
+    + apply Qclo, IH. lia.
+    + apply Qmatch, IH. lia.
+    + apply Qlist, Forall_forall=> t Hy.
+      apply (sum_list_with_in _ thunk_size) in Hy.
+      destruct t; simpl in *; try apply IH; lia.
+    + apply Qattr, map_Forall_lookup=> y t Hy.
+      apply (map_sum_with_lookup_le thunk_size) in Hy.
+      destruct t; simpl in *; try apply IH; lia.
+Qed.
+
+Lemma env_ind (P : env → Prop) :
+  (∀ E,
+    map_Forall (λ i, from_thunk (λ _, True) (λ E _, P E) (λ _ E _, P E) ∘ snd) E →
+    P E) →
+  ∀ E : env, P E.
+Proof. intros. apply (env_val_ind P (λ _, True)); auto. Qed.
+
+Lemma val_ind (Q : val → Prop) :
+  (∀ bl Hbl, Q (VLit bl Hbl)) →
+  (∀ x E e, Q (VClo x E e)) →
+  (∀ ms strict E e, Q (VCloMatch ms strict E e)) →
+  (∀ ts, Forall (from_thunk Q (λ _ _, True) (λ _ _ _, True)) ts → Q (VList ts)) →
+  (∀ ts,
+    map_Forall (λ _, from_thunk Q (λ _ _, True) (λ _ _ _, True)) ts → Q (VAttr ts)) →
+  (∀ v, Q v).
+Proof. intros. apply (env_val_ind (λ _, True) Q); auto. Qed.
+(** Correspondence to operational semantics *)
+Definition subst_env' (thunk_to_expr : thunk → expr) (E : env) : expr → expr :=
+  subst (prod_map id thunk_to_expr <$> E).
+
+Definition tattr_to_attr'
+    (thunk_to_expr : thunk → expr) (subst_env : env → expr → expr)
+    (E : env) (α : tattr) : attr :=
+  from_sum (AttrR ∘ subst_env E) (AttrN ∘ thunk_to_expr) α.
+
+Fixpoint thunk_to_expr (t : thunk) : expr :=
+  match t with
+  | Forced v => val_to_expr v
+  | Thunk E e => subst_env' thunk_to_expr E e
+  | Indirect x E tαs => ESelect
+      (EAttr (tattr_to_attr' thunk_to_expr (subst_env' thunk_to_expr) E <$> tαs)) x
+  end
+with val_to_expr (v : val) : expr :=
+  match v with
+  | VLit bl _ => ELit bl
+  | VClo x E e => EAbs x (subst_env' thunk_to_expr E e)
+  | VCloMatch E ms strict e => EAbsMatch
+      (fmap (M:=option) (subst_env' thunk_to_expr E) <$> ms)
+      strict
+      (subst_env' thunk_to_expr E e)
+  | VList ts => EList (thunk_to_expr <$> ts)
+  | VAttr ts => EAttr (AttrN ∘ thunk_to_expr <$> ts)
+  end.
+
+Notation subst_env := (subst_env' thunk_to_expr).
+Notation tattr_to_attr := (tattr_to_attr' thunk_to_expr subst_env).
+Notation attr_subst_env E := (attr_map (subst_env E)).
+
+Lemma subst_env_eq e E :
+  subst_env E e =
+    match e with
+    | ELit n => ELit n
+    | EId x mkd => EId x $
+        union_kinded (prod_map id thunk_to_expr <$> E !! x) mkd
+    | EAbs x e => EAbs x (subst_env E e)
+    | EAbsMatch ms strict e =>
+        EAbsMatch (fmap (M:=option) (subst_env E) <$> ms) strict (subst_env E e)
+    | EApp e1 e2 => EApp (subst_env E e1) (subst_env E e2)
+    | ESeq μ e1 e2 => ESeq μ (subst_env E e1) (subst_env E e2)
+    | EList es => EList (subst_env E <$> es)
+    | EAttr αs => EAttr (attr_subst_env E <$> αs)
+    | ELetAttr k e1 e2 => ELetAttr k (subst_env E e1) (subst_env E e2)
+    | EBinOp op e1 e2 => EBinOp op (subst_env E e1) (subst_env E e2)
+    | EIf e1 e2 e3 => EIf (subst_env E e1) (subst_env E e2) (subst_env E e3)
+    end.
+Proof. rewrite /subst_env. destruct e; by rewrite /= ?lookup_fmap. Qed.
+
+Lemma subst_env_alt E e : subst_env E e = subst (prod_map id thunk_to_expr <$> E) e.
+Proof. done. Qed.
+
+(* Use the unfolding lemmas, don't rely on conversion *)
+Opaque subst_env'.
+
+Lemma subst_env_empty e : subst_env ∅ e = e.
+Proof. rewrite subst_env_alt. apply subst_empty. Qed.
+
+Lemma final_val_to_expr v : final SHALLOW (val_to_expr v).
+Proof. induction v; simpl; constructor; auto. Qed.
+Local Hint Resolve final_val_to_expr | 0 : core.
+Lemma step_not_val_to_expr v e : val_to_expr v -{SHALLOW}-> e → False.
+Proof. intros []%step_not_final. done. Qed.
+
+Lemma final_force_deep n t v :
+  force_deep n t = mret v → final DEEP (val_to_expr v).
+Proof.
+  revert t v. induction n as [|n IH]; intros v w; [done|].
+  rewrite force_deep_S /=.
+  intros; destruct v; simplify_res; eauto using final.
+  + destruct (mapM _ _) as [[vs|]|] eqn:Hmap; simplify_res; eauto.
+    constructor. revert vs Hmap.
+    induction ts as [|t ts IHts]; intros; simplify_res; [by constructor|..].
+    destruct (interp_thunk _ _) as [[w|]|]; simplify_res.
+    destruct (force_deep _ _) as [[w'|]|] eqn:?; simplify_res.
+    destruct (mapM _ _) as [[ws|]|]; simplify_res; eauto.
+  + destruct (map_mapM_sorted _ _ _) as [[vs|]|] eqn:Hmap; simplify_res.
+    constructor; [done|].
+    revert vs Hmap. induction ts as [|x t ts ?? IHts]
+      using (map_sorted_ind attr_le); intros ts' Hts.
+    { rewrite map_mapM_sorted_empty in Hts; simplify_res. done. }
+    rewrite map_mapM_sorted_insert //= in Hts.
+    destruct (interp_thunk _ _) as [[w|]|] eqn:?; simplify_res.
+    destruct (force_deep _ _) as [[w'|]|] eqn:?; simplify_res.
+    destruct (map_mapM_sorted _ _ _) as [[ws|]|] eqn:Hmap; simplify_res.
+    rewrite !fmap_insert /=. apply map_Forall_insert_2, IHts; eauto.
+Qed.
+
+Lemma interp_bin_op_Some_1 op v1 f :
+  interp_bin_op op v1 = Some f →
+  ∃ Φ, sem_bin_op op (val_to_expr v1) Φ.
+Proof.
+  intros Hinterp. unfold interp_bin_op, interp_eq in *.
+  repeat (case_match || simplify_option_eq);
+    eexists; by repeat econstructor; eauto using final.
+Qed.
+
+Lemma interp_bin_op_Some_2 op v1 Φ :
+  sem_bin_op op (val_to_expr v1) Φ →
+  is_Some (interp_bin_op op v1).
+Proof.
+  unfold interp_bin_op; destruct v1; inv 1;
+    repeat (case_match || simplify_option_eq); eauto.
+  destruct (option_to_eq_Some _) as [[??]|] eqn:Ho; simplify_eq/=; eauto.
+  by rewrite H2 in Ho.
+Qed.
+
+Lemma interp_eq_list_correct ts1 ts2 :
+  thunk_to_expr (interp_eq_list ts1 ts2) =D=>
+  sem_eq_list (thunk_to_expr <$> ts1) (thunk_to_expr <$> ts2).
+Proof.
+  simpl.
+  remember (kmap (λ n : nat, String "1" (pretty n)) ((ABS,.) <$> map_seq 0 ts1) ∪
+    kmap (λ n : nat, String "2" (pretty n)) ((ABS,.) <$> map_seq 0 ts2))
+    as E eqn:HE.
+  assert (∀ (i : nat) t, ts1 !! i = Some t →
+    E !! String "1" (pretty (i + 0)) = Some (ABS, t)) as Hts1.
+  { intros x t Hxt. rewrite Nat.add_0_r.
+    rewrite HE lookup_union (lookup_kmap _) lookup_fmap.
+    rewrite lookup_map_seq_0 Hxt /= union_Some_l. done. }
+  assert (∀ (i : nat) t, ts2 !! i = Some t →
+    E !! String "2" (pretty (i + 0)) = Some (ABS, t)) as Hts2.
+  { intros x t Hxt. rewrite Nat.add_0_r.
+    rewrite HE lookup_union_r; last by apply (lookup_kmap_None _).
+    rewrite (lookup_kmap _) lookup_fmap lookup_map_seq_0 Hxt /=. done. }
+  clear HE. revert ts2 Hts1 Hts2. generalize 0.
+  induction ts1 as [|t1 ts1 IH]; intros n [|t2 ts2] Hts1 Hts2; csimpl; [done..|].
+  rewrite 4!subst_env_eq /= !(subst_env_eq (ELit _)) /=. rewrite /String.app.
+  rewrite (Hts1 0 t1) // (Hts2 0 t2) //=.
+  constructor; [repeat constructor| |done].
+  apply IH; intros i t; rewrite Nat.add_succ_r;
+    [apply (Hts1 (S i))|apply (Hts2 (S i))].
+Qed.
+
+Lemma interp_lt_list_correct ts1 ts2 :
+  thunk_to_expr (interp_lt_list ts1 ts2) =D=>
+  sem_lt_list (thunk_to_expr <$> ts1) (thunk_to_expr <$> ts2).
+Proof.
+  simpl.
+  remember (kmap (λ n : nat, String "1" (pretty n)) ((ABS,.) <$> map_seq 0 ts1) ∪
+    kmap (λ n : nat, String "2" (pretty n)) ((ABS,.) <$> map_seq 0 ts2))
+    as E eqn:HE.
+  assert (∀ (i : nat) t, ts1 !! i = Some t →
+    E !! String "1" (pretty (i + 0)) = Some (ABS, t)) as Hts1.
+  { intros x t Hxt. rewrite Nat.add_0_r.
+    rewrite HE lookup_union (lookup_kmap _) lookup_fmap.
+    rewrite lookup_map_seq_0 Hxt /= union_Some_l. done. }
+  assert (∀ (i : nat) t, ts2 !! i = Some t →
+    E !! String "2" (pretty (i + 0)) = Some (ABS, t)) as Hts2.
+  { intros x t Hxt. rewrite Nat.add_0_r.
+    rewrite HE lookup_union_r; last by apply (lookup_kmap_None _).
+    rewrite (lookup_kmap _) lookup_fmap lookup_map_seq_0 Hxt /=. done. }
+  clear HE. revert ts2 Hts1 Hts2. generalize 0.
+  induction ts1 as [|t1 ts1 IH]; intros n [|t2 ts2] Hts1 Hts2; csimpl; [done..|].
+  rewrite 4!subst_env_eq /= !(subst_env_eq (ELit _)) /=. rewrite /String.app.
+  rewrite (Hts1 0 t1) // (Hts2 0 t2) //=.
+  constructor; [repeat constructor..|].
+  rewrite 4!subst_env_eq /= !(subst_env_eq (ELit _)) /=.
+  rewrite (Hts1 0 t1) // (Hts2 0 t2) //=.
+  constructor; [repeat constructor| |done].
+  apply IH; intros i t; rewrite Nat.add_succ_r;
+    [apply (Hts1 (S i))|apply (Hts2 (S i))].
+Qed.
+
+Lemma interp_eq_attr_correct ts1 ts2 :
+  dom ts1 = dom ts2 →
+  thunk_to_expr (interp_eq_attr ts1 ts2) =D=>
+  sem_eq_attr (AttrN ∘ thunk_to_expr <$> ts1) (AttrN ∘ thunk_to_expr <$> ts2).
+Proof.
+  intros Hdom. simpl.
+  remember (kmap (String "1") ((ABS,.) <$> ts1) ∪
+    kmap (String "2") ((ABS,.) <$> ts2)) as E eqn:HE.
+  assert (map_Forall (λ x t, E !! String "1" x = Some (ABS, t)) ts1) as Hts1.
+  { intros x t Hxt.
+    rewrite HE lookup_union (lookup_kmap (String "1")) lookup_fmap.
+    by rewrite Hxt /= union_Some_l. }
+  assert (map_Forall (λ x t, E !! String "2" x = Some (ABS, t)) ts2) as Hts2.
+  { intros x t Hxt.
+    rewrite HE lookup_union_r; last by apply (lookup_kmap_None _).
+    by rewrite (lookup_kmap (String "2")) lookup_fmap Hxt. }
+  clear HE. revert ts2 Hdom Hts1 Hts2.
+  induction ts1 as [|x t1 ts1 Hts1x IH] using (map_sorted_ind attr_le);
+    intros ts2 Hdom Hts1 Hts2.
+  { apply symmetry, dom_empty_inv_L in Hdom as ->. done. }
+  rewrite dom_insert_L in Hdom.
+  assert (is_Some (ts2 !! x)) as [t2 Hxt2] by (apply elem_of_dom; set_solver).
+  assert (dom ts1 = dom (delete x ts2)).
+  { rewrite dom_delete_L -Hdom. apply not_elem_of_dom in Hts1x. set_solver. }
+  rewrite -(insert_delete ts2 x t2) //. rewrite -(insert_delete ts2 x t2) // in Hts2.
+  apply map_Forall_insert in Hts1 as [Hx1 Hts1]; last done.
+  apply map_Forall_insert in Hts2 as [Hx2 Hts2]; last by rewrite lookup_delete.
+  rewrite /sem_eq_attr !fmap_insert /=. erewrite <-insert_merge by done.
+  rewrite sem_and_attr_insert; first last.
+  { intros y. rewrite lookup_merge !lookup_fmap /is_Some.
+    destruct (ts1 !! y) eqn:? , (delete x ts2 !! y); naive_solver. }
+  { rewrite lookup_merge !lookup_fmap lookup_delete /=. by destruct (ts1 !! x). }
+  rewrite map_imap_insert sem_and_attr_insert; first last.
+  { intros y. rewrite map_lookup_imap /is_Some.
+    destruct (ts1 !! y) eqn:?; naive_solver. }
+  { by rewrite map_lookup_imap Hts1x. }
+  rewrite 4!subst_env_eq /= !(subst_env_eq (ELit _)) /= Hx1 Hx2 /=.
+  constructor; [|apply IHts1; by auto|done]. by do 2 constructor.
+Qed.
+
+Lemma interp_bin_op_Some_Some_1 op v1 f Φ v2 t3 :
+  interp_bin_op op v1 = Some f →
+  sem_bin_op op (val_to_expr v1) Φ →
+  f v2 = Some t3 →
+  ∃ e3, Φ (val_to_expr v2) e3 ∧ thunk_to_expr t3 =D=> e3.
+Proof.
+  unfold interp_bin_op, interp_eq, type_of_val, type_of_expr;
+    destruct v1, v2; inv 2; intros;
+    repeat match goal with
+    | _ => progress simplify_option_eq
+    | H : _ <$> _ = ∅ |- _ => apply fmap_empty_inv in H
+    | H : context [dom (_ <$> _)] |- _ => rewrite !dom_fmap_L in H
+    | H : context [length (_ <$> _)] |- _ => rewrite !length_fmap in H
+    | _ => case_match
+    | _ => eexists; split; [done|]
+    | _ => by apply interp_eq_list_correct
+    | _ => eexists; split; [|by apply: interp_lt_list_correct]
+    | _ => by apply: interp_eq_attr_correct
+    | _ => eexists; split; [|done]
+    | _ => split; [|done]
+    | _ => rewrite map_fmap_singleton
+    | _ => rewrite fmap_delete
+    | _ => rewrite subst_env_empty
+    | _ => rewrite fmap_app
+    | _ => rewrite lookup_fmap
+    | _ => by constructor
+    end; eauto using final.
+  - apply reflexive_eq. f_equal. apply map_eq=> x.
+    rewrite !lookup_fmap. by destruct (_ !! _) as [[]|].
+  - by destruct (ts !! _).
+  - apply (map_minimal_key_Some _) in H as [[t Hx] ?].
+    split; [done|]. right. eexists s, _; split_and!.
+    + by rewrite lookup_fmap Hx.
+    + intros y. rewrite lookup_fmap fmap_is_Some. auto.
+    + rewrite 3!fmap_insert map_fmap_singleton /=.
+      by rewrite lookup_total_alt Hx fmap_delete.
+  - apply map_minimal_key_None in H as ->. auto.
+  - split; [done|]. by rewrite map_fmap_union.
+Qed.
+
+Lemma interp_bin_op_Some_Some_2 op v1 f Φ v2 e3 :
+  interp_bin_op op v1 = Some f →
+  sem_bin_op op (val_to_expr v1) Φ →
+  Φ (val_to_expr v2) e3 →
+  ∃ t3, f v2 = Some t3 ∧ thunk_to_expr t3 =D=> e3.
+Proof.
+  unfold interp_bin_op, interp_eq; destruct v1; inv 2; intros;
+    repeat match goal with
+    | H : ∃ _, _ |- _ => destruct H
+    | H : _ ∧ _ |- _ => destruct H
+    | H : _ <$> _ = ∅ |- _ => apply fmap_empty_inv in H
+    | H : context [(_ <$> _) !! _ = _] |- _ => rewrite lookup_fmap in H
+    | H : context [dom (_ <$> _)] |- _ => rewrite !dom_fmap_L in H
+    | H : context [length (_ <$> _)] |- _ => rewrite !length_fmap in H
+    | _ => progress simplify_option_eq
+    | H : val_to_expr ?v2 = _ |- _ => destruct v2
+    | _ => case_match
+    | _ => eexists; split; [|by apply interp_eq_attr_correct]
+    | _ => eexists; split; [|by apply interp_eq_list_correct]
+    | _ => eexists; split; [|by apply interp_lt_list_correct]
+    | _ => eexists; split; [done|]
+    | _ => rewrite map_fmap_singleton
+    | _ => rewrite fmap_delete
+    | _ => rewrite subst_env_empty
+    | _ => rewrite fmap_app
+    | _ => rewrite map_fmap_union
+    end; eauto.
+  - rewrite (option_to_eq_Some_Some _ _ H1) /=. by eexists.
+  - apply reflexive_eq. f_equal. apply map_eq=> x.
+    rewrite !lookup_fmap. by destruct (_ !! _) as [[]|].
+  - rewrite lookup_fmap. by destruct (_ !! _).
+  - destruct H1 as [[Hemp _]|(x & e' & Hx & Hleast & ->)].
+    { by apply fmap_empty_inv in Hemp as ->. }
+    rewrite lookup_fmap fmap_Some in Hx. destruct Hx as (t & Hx & [= ->]).
+    setoid_rewrite lookup_fmap in Hleast. setoid_rewrite fmap_is_Some in Hleast.
+    apply (map_minimal_key_Some _) in H as [??].
+    assert (s = x) as -> by (apply (anti_symm attr_le); naive_solver).
+    rewrite 3!fmap_insert map_fmap_singleton /= fmap_delete.
+    rewrite lookup_total_alt Hx. done.
+  - apply map_minimal_key_None in H as ->. naive_solver.
+Qed.
+
+Lemma interp_match_subst E ts ms strict :
+  interp_match ts (fmap (M:=option) (subst_env E) <$> ms) strict =
+  fmap (M:=gmap string) (sum_map (subst_env E) id) <$> interp_match ts ms strict.
+Proof.
+  unfold interp_match. set (f mt mme := match mt with _ => _ end).
+  revert ts. induction ms as [|x mt ms Hmsx IH] using map_ind; intros ts.
+  { rewrite fmap_empty merge_empty_r.
+    induction ts as [|x t ts Hmsx IH] using map_ind; [done|].
+    rewrite omap_insert /=. destruct strict; simplify_eq/=.
+    { rewrite map_mapM_insert_option //= lookup_omap Hmsx. done. }
+    rewrite -omap_delete delete_notin //. }
+  destruct (ts !! x) as [t|] eqn:Htsx.
+  { rewrite -(insert_delete ts x t) // fmap_insert.
+    rewrite -!(insert_merge _ _ _ _ (Some (inr t))) //.
+    rewrite !map_mapM_insert_option /=;
+      [|by rewrite lookup_merge lookup_delete ?lookup_fmap Hmsx..].
+    rewrite IH. destruct (map_mapM id _); rewrite /= ?fmap_insert //. }
+  rewrite -(insert_merge_r _ _ _ _ (inl <$> mt)) /=; last first.
+  { rewrite Htsx /=. by destruct mt. }
+  rewrite fmap_insert.
+  rewrite -(insert_merge_r _ _ _ _ (inl <$> (subst_env E <$> mt))) /=; last first.
+  { rewrite Htsx /=. by destruct mt. }
+    rewrite !map_mapM_insert_option /=;
+      [|by rewrite lookup_merge ?lookup_fmap Htsx Hmsx..].
+  rewrite IH. destruct mt, (map_mapM id _); rewrite /= ?fmap_insert //.
+Qed.
+
+Lemma interp_match_Some_1 ts ms strict tαs :
+  interp_match ts ms strict = Some tαs →
+  matches (thunk_to_expr <$> ts) ms strict (tattr_to_attr ∅ <$> tαs).
+Proof.
+  unfold interp_match. set (f mt mme := match mt with _ => _ end).
+  revert ts tαs.
+  induction ms as [|x mt ms Hmsx IH] using map_ind; intros ts αs Hmatch.
+  { rewrite merge_empty_r in Hmatch. revert αs Hmatch.
+    induction ts as [|x t ts Hmsx IH] using map_ind; intros ts' Hmatch.
+    { rewrite omap_empty map_mapM_empty in Hmatch. injection Hmatch as <-.
+      rewrite !fmap_empty. constructor. }
+    rewrite omap_insert /= in Hmatch. destruct strict; simplify_eq/=.
+    { rewrite map_mapM_insert_option //= in Hmatch. by rewrite lookup_omap Hmsx. }
+    rewrite fmap_insert.
+    rewrite -omap_delete delete_notin // in Hmatch. apply IH in Hmatch.
+    apply matches_strict; rewrite ?lookup_fmap ?Hmsx; eauto. }
+  destruct (ts !! x) as [t|] eqn:Htsx.
+  { rewrite -(insert_delete ts x t) //.
+    rewrite -(insert_delete ts x t) // in Hmatch.
+    rewrite -(insert_merge _ _ _ _ (Some (inr t))) // in Hmatch.
+    rewrite map_mapM_insert_option /= in Hmatch;
+      last (by rewrite lookup_merge lookup_delete Hmsx).
+    destruct (map_mapM id _) as [E''|] eqn:?; simplify_eq/=.
+    injection Hmatch as <-.
+    rewrite !fmap_insert /=. constructor.
+    - by rewrite lookup_fmap lookup_delete.
+    - done.
+    - by apply IH. }
+  rewrite -(insert_merge_r _ _ _ _ (inl <$> mt)) /= in Hmatch; last first.
+  { rewrite Htsx /=. by destruct mt. }
+  rewrite map_mapM_insert_option /= in Hmatch;
+    last (by rewrite lookup_merge Htsx Hmsx).
+  destruct mt as [t|]; simplify_eq/=.
+  destruct (map_mapM id _) as [E''|] eqn:?; simplify_eq/=.
+  injection Hmatch as <-. rewrite !fmap_insert /= subst_env_empty. constructor.
+  - by rewrite lookup_fmap Htsx.
+  - done.
+  - by apply IH.
+Qed.
+
+Lemma interp_match_Some_2 es ms strict αs :
+  matches es ms strict αs →
+  interp_match (Thunk ∅ <$> es) ms strict = Some (attr_to_tattr ∅ <$> αs).
+Proof.
+  unfold interp_match. set (f mt mme := match mt with _ => _ end).
+  induction 1; [done|..].
+  - rewrite fmap_empty merge_empty_r.
+    induction es as [|x e es ? IH] using map_ind; [done|].
+    rewrite fmap_insert omap_insert /= -omap_delete -fmap_delete delete_notin //.
+  - rewrite !fmap_insert /=.
+    rewrite -(insert_merge _ _ _ _ (Some (inr (Thunk ∅ e)))) //.
+    rewrite map_mapM_insert_option /=; last first.
+    { by rewrite lookup_merge !lookup_fmap H H0. }
+    by rewrite IHmatches.
+  - rewrite !fmap_insert /=.
+    rewrite -(insert_merge_r _ _ _ _ (Some (inl d))) /=; last first.
+    { by rewrite lookup_fmap H. }
+    rewrite map_mapM_insert_option /=; last first.
+    { by rewrite lookup_merge !lookup_fmap H H0. }
+    by rewrite IHmatches /=.
+Qed.
+
+Lemma force_deep_le {n1 n2 v mv} :
+  force_deep n1 v = Res mv → n1 ≤ n2 → force_deep n2 v = Res mv
+with interp_le {n1 n2 E e mv} :
+  interp n1 E e = Res mv → n1 ≤ n2 → interp n2 E e = Res mv
+with interp_thunk_le {n1 n2 t mvs} :
+  interp_thunk n1 t = Res mvs → n1 ≤ n2 → interp_thunk n2 t = Res mvs
+with interp_app_le {n1 n2 v t mv} :
+  interp_app n1 v t = Res mv → n1 ≤ n2 → interp_app n2 v t = Res mv.
+Proof.
+  - destruct n1 as [|n1], n2 as [|n2]; intros Ht ?; [done || lia..|].
+    rewrite force_deep_S in Ht; rewrite force_deep_S; simpl in *.
+    destruct v as []; simplify_res; try done.
+    + destruct (mapM _ _) as [mvs|] eqn:Hmap; simplify_res.
+      erewrite mapM_Res_impl; [done..|]. intros t mw Hinterp; simpl in *.
+      destruct (interp_thunk n1 _) as [mw'|] eqn:Hinterp'; simplify_res.
+      rewrite (interp_thunk_le _ _ _ _ Hinterp') /=; last lia.
+      destruct mw'; simplify_res; eauto with lia.
+    + destruct (map_mapM_sorted _ _ _) eqn:?; simplify_res.
+      erewrite (map_mapM_sorted_Res_impl attr_le); [done..|].
+      clear dependent ts. intros t mw Hinterp; simpl in *.
+      destruct (interp_thunk n1 _) as [mw'|] eqn:Hinterp'; simplify_res.
+      rewrite (interp_thunk_le _ _ _ _ Hinterp') /=; last lia.
+      destruct mw'; simplify_res; eauto with lia.
+  - destruct n1 as [|n1], n2 as [|n2]; intros He ?; [done || lia..|].
+    rewrite interp_S in He; rewrite interp_S; destruct e;
+      repeat match goal with
+      | _ => case_match
+      | H : context [(_ <$> ?mx)] |- _ => destruct mx eqn:?; simplify_res
+      | H : ?r ≫= _ = _ |- _ => destruct r as [[]|] eqn:?; simplify_res
+      | H : _ <$> ?r = _ |- _ => destruct r as [[]|] eqn:?; simplify_res
+      | H : interp ?n' _ _ = Res ?mv |- interp ?n ?E ?e ≫= _ = _ =>
+        rewrite (interp_le n' n E e mv); [|done || lia..]
+      | H : interp_app ?n' _ _ = Res ?mv |- interp_app ?n ?E ?e ≫= _ = _ =>
+        rewrite (interp_app_le n' n E e mv); [|done || lia..]
+      | H : force_deep ?n' _ = Res ?mv |- force_deep ?n ?t ≫= _ = _ =>
+        rewrite (force_deep_le n' n t mv); [|done || lia..]
+      | _ => progress simplify_res
+      | _ => progress simplify_option_eq
+      end; eauto with lia.
+  - destruct n1 as [|n1], n2 as [|n2]; intros He ?; [by (done || lia)..|].
+    rewrite interp_thunk_S in He. rewrite interp_thunk_S.
+    destruct t; repeat (case_match || destruct (_ !! _)
+                        || simplify_res); eauto with lia.
+  - destruct n1 as [|n1], n2 as [|n2]; intros He ?; [by (done || lia)..|].
+    rewrite interp_app_S /= in He; rewrite interp_app_S /=.
+    destruct v; simplify_res; eauto with lia.
+    + destruct (interp_thunk n1 t) as [mw|] eqn:?; simplify_res.
+      erewrite interp_thunk_le by eauto with lia. simpl.
+      destruct mw as [w|]; simplify_res; [|done].
+      destruct (maybe VAttr w) as [ts|]; simplify_res; [|done].
+      destruct (interp_match _ _ _); simplify_res; eauto with lia.
+    + destruct (_ !! "__functor") as [tf|]; simplify_res; [|done].
+      destruct (interp_thunk n1 tf) as [mw|] eqn:?; simplify_res.
+      erewrite interp_thunk_le by eauto with lia. simpl.
+      destruct mw as [w|]; simplify_res; [|done].
+      destruct (interp_app n1 _ _) as [mw|] eqn:?; simplify_res.
+      erewrite interp_app_le by eauto with lia; simpl.
+      destruct mw; simplify_res; eauto with lia.
+Qed.
+
+Lemma mapM_interp_le {n1 n2 ts mvs} :
+  mapM (mbind (force_deep n1) ∘ interp_thunk n1) ts = Res mvs →
+  n1 ≤ n2 →
+  mapM (mbind (force_deep n2) ∘ interp_thunk n2) ts = Res mvs.
+Proof.
+  intros. eapply mapM_Res_impl; [done|]; simpl; intros t mv ?.
+  destruct (interp_thunk _ _) as [mw|] eqn:Hthunk; simplify_res.
+  rewrite (interp_thunk_le Hthunk) //=.
+  destruct mw; simplify_res; eauto using force_deep_le.
+Qed.
+Lemma map_mapM_interp_le {n1 n2 ts mvs} :
+  map_mapM_sorted attr_le (mbind (force_deep n1) ∘ interp_thunk n1) ts = Res mvs →
+  n1 ≤ n2 →
+  map_mapM_sorted attr_le (mbind (force_deep n2) ∘ interp_thunk n2) ts = Res mvs.
+Proof.
+  intros. eapply (map_mapM_sorted_Res_impl attr_le); [done|]; simpl.
+  intros t mv ?. destruct (interp_thunk _ _) as [mw|] eqn:Hthunk; simplify_res.
+  rewrite (interp_thunk_le Hthunk) //=.
+  destruct mw; simplify_res; eauto using force_deep_le.
+Qed.
+
+Lemma interp_agree {n1 n2 E e mv1 mv2} :
+  interp n1 E e = Res mv1 → interp n2 E e = Res mv2 → mv1 = mv2.
+Proof.
+  intros He1 He2. apply (inj Res). destruct (total (≤) n1 n2).
+  - rewrite -He2. symmetry. eauto using interp_le.
+  - rewrite -He1. eauto using interp_le.
+Qed.
+
+Lemma subst_env_union E1 E2 e :
+  subst_env (union_kinded E1 E2) e = subst_env E1 (subst_env E2 e).
+Proof.
+  rewrite !subst_env_alt -subst_union. f_equal. apply map_eq=> x.
+  rewrite lookup_union_with !lookup_fmap lookup_union_with.
+  by repeat destruct (_ !! _) as [[[]]|].
+Qed.
+
+Lemma union_kinded_union {A} (E1 E2 : gmap string (kind * A)) :
+  map_Forall (λ _ ka, ka.1 = ABS) E1 → union_kinded E1 E2 = E1 ∪ E2.
+Proof.
+  rewrite map_Forall_lookup; intros.
+  apply map_eq=> x. rewrite lookup_union_with lookup_union.
+  destruct (E1 !! x) as [[[] a]|] eqn:?; naive_solver.
+Qed.
+
+Lemma subst_abs_env_insert E x e t :
+  subst_env (<[x:=(ABS, t)]> E) e
+  = subst {[x:=(ABS, thunk_to_expr t)]} (subst_env E e).
+Proof.
+  assert (<[x:=(ABS, t)]> E =
+    union_kinded {[x:=(ABS, t)]} E) as ->.
+  { apply map_eq=> y. rewrite lookup_union_with.
+    destruct (decide (x = y)) as [->|].
+    - rewrite lookup_insert lookup_singleton /=. by destruct (_ !! _).
+    - rewrite lookup_insert_ne // lookup_singleton_ne //. by destruct (_ !! _). }
+  rewrite subst_env_union subst_env_alt. by rewrite map_fmap_singleton.
+Qed.
+
+Lemma subst_abs_as_subst_env x e1 e2 :
+  subst {[x:=(ABS, e2)]} e1 = subst_env (<[x:=(ABS, Thunk ∅ e2)]> ∅) e1.
+Proof. rewrite subst_abs_env_insert //= !subst_env_empty //. Qed.
+
+Lemma subst_env_insert_proper e1 e2 E1 E2 x t1 t2 :
+  subst_env E1 e1 = subst_env E2 e2 →
+  thunk_to_expr t1 = thunk_to_expr t2 →
+  subst_env (<[x:=(ABS, t1)]> E1) e1 = subst_env (<[x:=(ABS, t2)]> E2) e2.
+Proof. rewrite !subst_abs_env_insert //. auto with f_equal. Qed.
+
+Lemma subst_env_insert_proper' e1 e2 E1 E2 x E1' E2' e1' e2' :
+  subst_env E1 e1 = subst_env E2 e2 →
+  subst_env E1' e1' = subst_env E2' e2' →
+  subst_env (<[x:=(ABS, Thunk E1' e1')]> E1) e1
+  = subst_env (<[x:=(ABS, Thunk E2' e2')]> E2) e2.
+Proof. intros. by apply subst_env_insert_proper. Qed.
+
+Lemma subst_env_union_fmap_proper k e1 e2 E1 E2 ts1 ts2 :
+  subst_env E1 e1 = subst_env E2 e2 →
+  AttrN ∘ thunk_to_expr <$> ts1 = AttrN ∘ thunk_to_expr <$> ts2 →
+  subst_env (union_kinded ((k,.) <$> ts1) E1) e1
+  = subst_env (union_kinded ((k,.) <$> ts2) E2) e2.
+Proof.
+  intros He Hes. rewrite !subst_env_union; [|by apply env_unionable_with..].
+  rewrite He !subst_env_alt /=. f_equal.
+  apply map_eq=> x. rewrite !lookup_fmap.
+  apply (f_equal (.!! x)) in Hes. rewrite !lookup_fmap in Hes.
+  destruct (ts1 !! x), (ts2 !! x); simplify_eq/=; auto with f_equal.
+Qed.
+
+Lemma subst_env_fmap_proper k e ts1 ts2 :
+  AttrN ∘ thunk_to_expr <$> ts1 = AttrN ∘ thunk_to_expr <$> ts2 →
+  subst_env ((k,.) <$> ts1) e = subst_env ((k,.) <$> ts2) e.
+Proof.
+  intros. rewrite -(right_id_L ∅ (union_kinded) (_ <$> ts1))
+    -(right_id_L ∅ (union_kinded) (_ <$> ts2)).
+  by apply subst_env_union_fmap_proper.
+Qed.
+
+Lemma tattr_to_attr_from_attr E (αs : gmap string attr) :
+  tattr_to_attr E <$> (attr_to_tattr E <$> αs) = attr_subst_env E <$> αs.
+Proof.
+  apply map_eq=> x. rewrite /tattr_to_attr !lookup_fmap.
+  destruct (αs !! x) as [[[] ]|] eqn:?; auto.
+Qed.
+
+Lemma tattr_to_attr_from_attr_empty (αs : gmap string attr) :
+  tattr_to_attr ∅ <$> (attr_to_tattr ∅ <$> αs) = αs.
+Proof.
+  rewrite tattr_to_attr_from_attr. apply map_eq=> x. rewrite !lookup_fmap.
+  destruct (αs !! x) as [[[] ]|] eqn:?; f_equal/=; by rewrite subst_env_empty.
+Qed.
+
+Lemma indirects_env_proper E1 E2 tαs1 tαs2 e1 e2 :
+  tattr_to_attr E1 <$> tαs1 = tattr_to_attr E2 <$> tαs2 →
+  subst_env E1 e1 = subst_env E2 e2 →
+  subst_env (indirects_env E1 tαs1) e1 = subst_env (indirects_env E2 tαs2) e2.
+Proof.
+  intros Htαs HE. rewrite /indirects_env -!union_kinded_union;
+    [|intros ??; rewrite map_lookup_imap=> ?; by simplify_option_eq..].
+  rewrite !subst_env_union HE !subst_env_alt. f_equal.
+  apply map_eq=> x. rewrite !lookup_fmap !map_lookup_imap.
+  pose proof (f_equal (.!! x) Htαs) as Hx. rewrite !lookup_fmap in Hx.
+  repeat destruct (_ !! x) as [[]|]; simplify_eq/=; auto with f_equal.
+Qed.
+
+Lemma subst_env_indirects_env E tαs e :
+  subst_env (indirects_env E tαs) e
+  = subst_env (indirects_env ∅ (attr_to_tattr ∅ <$> (tattr_to_attr E <$> tαs)))
+    (subst_env E e).
+Proof.
+  rewrite /indirects_env -!union_kinded_union;
+    [|intros ??; rewrite map_lookup_imap=> ?; by simplify_option_eq..].
+  rewrite !subst_env_union subst_env_empty !subst_env_alt.
+  f_equal. apply map_eq=> x. rewrite !lookup_fmap !map_lookup_imap !lookup_fmap.
+  destruct (_ !! _) as [[]|];
+    do 4 f_equal/=; auto using tattr_to_attr_from_attr_empty.
+Qed.
+
+Lemma subst_env_indirects_env_attr_to_tattr E αs e :
+  subst_env (indirects_env E (attr_to_tattr E <$> αs)) e
+  = subst (indirects (attr_subst_env E <$> αs)) (subst_env E e).
+Proof.
+  rewrite /indirects_env -!union_kinded_union;
+    [|intros ??; rewrite map_lookup_imap=> ?; by simplify_option_eq..].
+  rewrite subst_env_union !subst_env_alt. f_equal.
+  apply map_eq=> x. rewrite !lookup_fmap !map_lookup_imap !lookup_fmap.
+  repeat destruct (_ !! x) as [[]|]; simplify_eq/=; do 4 f_equal/=.
+  by rewrite tattr_to_attr_from_attr.
+Qed.
+
+Lemma subst_env_indirects_env_attr_to_tattr_empty αs e :
+  subst_env (indirects_env ∅ (attr_to_tattr ∅ <$> αs)) e =
+  subst (indirects αs) e.
+Proof.
+  rewrite subst_env_indirects_env_attr_to_tattr subst_env_empty. do 3 f_equal.
+  apply map_eq=> x. rewrite !lookup_fmap.
+  destruct (_ !! x) as [[]|]; do 2 f_equal/=; auto using subst_env_empty.
+Qed.
+
+Lemma interp_val_to_expr E e v :
+  subst_env E e = val_to_expr v →
+  ∃ w m, interp m E e = mret w ∧ val_to_expr v = val_to_expr w.
+Proof.
+  revert v. induction e; intros [];
+    rewrite subst_env_eq; intros; simplify_eq/=.
+  - eexists (VLit _ ltac:(done)), 1. split; [|done]. by rewrite interp_lit.
+  - eexists (VClo _ _ _), 1. rewrite interp_S /=. auto with f_equal.
+  - eexists (VCloMatch _ _ _ _), 1. rewrite interp_S /=. auto with f_equal.
+  - eexists (VList _), 1. rewrite interp_S /=. split; [done|].
+    f_equal. rewrite -H0. clear.
+    induction es; f_equal/=; auto.
+  - eexists (VAttr _), 1. rewrite interp_S /=. split; [done|].
+    assert (no_recs αs) as Hrecs.
+    { intros y α Hy.
+      apply (f_equal (.!! y)) in H0. rewrite !lookup_fmap Hy /= in H0.
+      destruct (ts !! y), α; by simplify_eq/=. }
+    rewrite from_attr_no_recs // -H0.
+    f_equal. apply map_eq=> y.
+    rewrite !lookup_fmap. destruct (αs !! y) as [[]|] eqn:?; do 2 f_equal/=.
+    eauto using no_recs_lookup.
+Qed.
+
+Lemma interp_val_to_expr_Res m E e v mw :
+  subst_env E e = val_to_expr v →
+  interp m E e = Res mw →
+  Some (val_to_expr v) = val_to_expr <$> mw.
+Proof.
+  intros (mw' & m' & Hinterp' & ->)%interp_val_to_expr Hinterp.
+  by assert (mw = Some mw') as -> by eauto using interp_agree.
+Qed.
+
+Lemma interp_empty_val_to_expr v :
+  ∃ w m, interp m ∅ (val_to_expr v) = mret w ∧ val_to_expr v = val_to_expr w.
+Proof. apply interp_val_to_expr. by rewrite subst_env_empty. Qed.
+
+Lemma interp_empty_val_to_expr_Res m v mw :
+  interp m ∅ (val_to_expr v) = Res mw →
+  Some (val_to_expr v) = val_to_expr <$> mw.
+Proof. apply interp_val_to_expr_Res. by rewrite subst_env_empty. Qed.
+
+Lemma interp_eq_list_proper ts1 ts2 ts1' ts2' :
+  thunk_to_expr <$> ts1 = thunk_to_expr <$> ts1' →
+  thunk_to_expr <$> ts2 = thunk_to_expr <$> ts2' →
+  thunk_to_expr (interp_eq_list ts1 ts2)
+  = thunk_to_expr (interp_eq_list ts1' ts2').
+Proof.
+  intros Hts1 Hts2. rewrite /= !subst_env_alt.
+  f_equal; last first.
+  { revert ts1' ts2 ts2' Hts1 Hts2. generalize 0.
+    induction ts1; intros ? [] [] [] ??; simplify_eq/=; auto with f_equal. }
+  rewrite !map_fmap_union. f_equal; apply map_eq=> y; rewrite !lookup_fmap.
+  - destruct (kmap _ _ !! y) as [[k e]|] eqn:Hy; simplify_eq/=.
+    + apply (lookup_kmap_Some _) in Hy as (y' & -> & Hy).
+      rewrite (lookup_kmap _) lookup_fmap lookup_map_seq_0.
+      rewrite lookup_fmap lookup_map_seq_0 in Hy.
+      apply (f_equal (.!! y')) in Hts1. rewrite !list_lookup_fmap in Hts1.
+      repeat destruct (_ !! _); simplify_eq/=; auto with f_equal.
+    + rewrite lookup_kmap_None in Hy.
+      apply symmetry, fmap_None, (lookup_kmap_None _).
+      intros y' ->. generalize (Hy _ eq_refl).
+      rewrite !lookup_fmap !lookup_map_seq_0.
+      apply (f_equal (.!! y')) in Hts1. rewrite !list_lookup_fmap in Hts1.
+      intros. repeat destruct (_ !! _); by simplify_eq/=.
+  - destruct (kmap _ _ !! y) as [[k e]|] eqn:Hy; simplify_eq/=.
+    + apply (lookup_kmap_Some _) in Hy as (y' & -> & Hy).
+      rewrite (lookup_kmap _) lookup_fmap lookup_map_seq_0.
+      rewrite lookup_fmap lookup_map_seq_0 in Hy.
+      apply (f_equal (.!! y')) in Hts2. rewrite !list_lookup_fmap in Hts2.
+      repeat destruct (_ !! _); simplify_eq/=; auto with f_equal.
+    + rewrite lookup_kmap_None in Hy.
+      apply symmetry, fmap_None, (lookup_kmap_None _).
+      intros y' ->. generalize (Hy _ eq_refl).
+      rewrite !lookup_fmap !lookup_map_seq_0.
+      apply (f_equal (.!! y')) in Hts2. rewrite !list_lookup_fmap in Hts2.
+      intros. repeat destruct (_ !! _); by simplify_eq/=.
+Qed.
+
+Lemma interp_lt_list_proper ts1 ts2 ts1' ts2' :
+  thunk_to_expr <$> ts1 = thunk_to_expr <$> ts1' →
+  thunk_to_expr <$> ts2 = thunk_to_expr <$> ts2' →
+  thunk_to_expr (interp_lt_list ts1 ts2)
+  = thunk_to_expr (interp_lt_list ts1' ts2').
+Proof.
+  intros Hts1 Hts2. rewrite /= !subst_env_alt.
+  f_equal; last first.
+  { revert ts1' ts2 ts2' Hts1 Hts2. generalize 0.
+    induction ts1; intros ? [] [] [] ??; simplify_eq/=; auto with f_equal. }
+  rewrite !map_fmap_union. f_equal; apply map_eq=> y; rewrite !lookup_fmap.
+  - destruct (kmap _ _ !! y) as [[k e]|] eqn:Hy; simplify_eq/=.
+    + apply (lookup_kmap_Some _) in Hy as (y' & -> & Hy).
+      rewrite (lookup_kmap _) lookup_fmap lookup_map_seq_0.
+      rewrite lookup_fmap lookup_map_seq_0 in Hy.
+      apply (f_equal (.!! y')) in Hts1. rewrite !list_lookup_fmap in Hts1.
+      repeat destruct (_ !! _); simplify_eq/=; auto with f_equal.
+    + rewrite lookup_kmap_None in Hy.
+      apply symmetry, fmap_None, (lookup_kmap_None _).
+      intros y' ->. generalize (Hy _ eq_refl).
+      rewrite !lookup_fmap !lookup_map_seq_0.
+      apply (f_equal (.!! y')) in Hts1. rewrite !list_lookup_fmap in Hts1.
+      intros. repeat destruct (_ !! _); by simplify_eq/=.
+  - destruct (kmap _ _ !! y) as [[k e]|] eqn:Hy; simplify_eq/=.
+    + apply (lookup_kmap_Some _) in Hy as (y' & -> & Hy).
+      rewrite (lookup_kmap _) lookup_fmap lookup_map_seq_0.
+      rewrite lookup_fmap lookup_map_seq_0 in Hy.
+      apply (f_equal (.!! y')) in Hts2. rewrite !list_lookup_fmap in Hts2.
+      repeat destruct (_ !! _); simplify_eq/=; auto with f_equal.
+    + rewrite lookup_kmap_None in Hy.
+      apply symmetry, fmap_None, (lookup_kmap_None _).
+      intros y' ->. generalize (Hy _ eq_refl).
+      rewrite !lookup_fmap !lookup_map_seq_0.
+      apply (f_equal (.!! y')) in Hts2. rewrite !list_lookup_fmap in Hts2.
+      intros. repeat destruct (_ !! _); by simplify_eq/=.
+Qed.
+
+Lemma interp_eq_attr_proper ts1 ts2 ts1' ts2' :
+  thunk_to_expr <$> ts1 = thunk_to_expr <$> ts1' →
+  thunk_to_expr <$> ts2 = thunk_to_expr <$> ts2' →
+  thunk_to_expr (interp_eq_attr ts1 ts2)
+  = thunk_to_expr (interp_eq_attr ts1' ts2').
+Proof.
+  intros Hts1 Hts2. rewrite /= !subst_env_alt.
+  f_equal; last first.
+  { clear Hts2. f_equal. apply map_eq=> y.
+    rewrite !map_lookup_imap. apply (f_equal (.!! y)) in Hts1.
+    rewrite !lookup_fmap in Hts1. by repeat destruct (_ !! _). }
+  rewrite !map_fmap_union. f_equal; apply map_eq=> y; rewrite !lookup_fmap.
+  - destruct (kmap _ _ !! y) as [[k e]|] eqn:Hy; simplify_eq/=.
+    + apply (lookup_kmap_Some _) in Hy as (y' & -> & Hy).
+      rewrite (lookup_kmap (String "1")) lookup_fmap.
+      rewrite lookup_fmap in Hy.
+      apply (f_equal (.!! y')) in Hts1. rewrite !lookup_fmap in Hts1.
+      repeat destruct (_ !! _); simplify_eq/=; auto with f_equal.
+    + rewrite lookup_kmap_None in Hy.
+      apply symmetry, fmap_None, (lookup_kmap_None _).
+      intros y' ->. generalize (Hy _ eq_refl). rewrite !lookup_fmap.
+      apply (f_equal (.!! y')) in Hts1. rewrite !lookup_fmap in Hts1.
+      intros. repeat destruct (_ !! _); by simplify_eq/=.
+  - destruct (kmap _ _ !! y) as [[k e]|] eqn:Hy; simplify_eq/=.
+    + apply (lookup_kmap_Some _) in Hy as (y' & -> & Hy).
+      rewrite (lookup_kmap (String "2")) lookup_fmap.
+      rewrite lookup_fmap in Hy.
+      apply (f_equal (.!! y')) in Hts2. rewrite !lookup_fmap in Hts2.
+      repeat destruct (_ !! _); simplify_eq/=; auto with f_equal.
+    + rewrite lookup_kmap_None in Hy.
+      apply symmetry, fmap_None, (lookup_kmap_None _).
+      intros y' ->. generalize (Hy _ eq_refl). rewrite !lookup_fmap.
+      apply (f_equal (.!! y')) in Hts2. rewrite !lookup_fmap in Hts2.
+      intros. repeat destruct (_ !! _); by simplify_eq/=.
+Qed.
+
+Opaque interp_eq_list interp_lt_list interp_eq_attr.
+
+Lemma interp_bin_op_proper op v1 v2 :
+  val_to_expr v1 = val_to_expr v2 →
+  match interp_bin_op op v1, interp_bin_op op v2 with
+  | None, None => True
+  | Some f1, Some f2 => ∀ v1' v2',
+     val_to_expr v1' = val_to_expr v2' →
+     thunk_to_expr <$> f1 v1' = thunk_to_expr <$> f2 v2'
+  | _, _ => False
+  end.
+Proof.
+  intros. unfold interp_bin_op, interp_eq;
+    repeat (done || case_match || simplify_eq/= || 
+      destruct (option_to_eq_Some _) as [[]|]);
+    intros [] [] ?; simplify_eq/=;
+    repeat match goal with
+    | _ => done
+    | _ => progress simplify_option_eq
+    | _ => rewrite map_fmap_singleton
+    | _ => rewrite map_fmap_union
+    | _ => case_match
+    | |- context[ maybe _ ?x ] => is_var x; destruct x
+    end; auto with congruence.
+  - f_equal. by apply interp_eq_list_proper.
+  - apply (f_equal length) in H, H0. rewrite !length_fmap in H H0. congruence.
+  - apply (f_equal length) in H, H0. rewrite !length_fmap in H H0. congruence.
+  - f_equal. apply interp_eq_attr_proper.
+    + rewrite 2!map_fmap_compose in H. by simplify_eq.
+    + rewrite 2!map_fmap_compose in H0. by simplify_eq.
+  - apply (f_equal dom) in H, H0. rewrite !dom_fmap_L in H H0. congruence.
+  - apply (f_equal dom) in H, H0. rewrite !dom_fmap_L in H H0. congruence.
+  - destruct v1, v2; by simplify_eq/=.
+  - repeat destruct (option_to_eq_Some _) as [[]|]; simplify_eq/=; auto.
+  - do 3 f_equal. apply map_eq=> y. rewrite !lookup_fmap.
+    apply (f_equal (.!! y)) in H. rewrite !lookup_fmap in H.
+    repeat destruct (_ !! _) as [[]|]; naive_solver.
+  - f_equal. by apply interp_lt_list_proper.
+  - rewrite !fmap_insert /=. auto 10 with f_equal.
+  - by rewrite !fmap_app H0 H.
+  - apply (f_equal (.!! s)) in H. rewrite !lookup_fmap in H.
+    repeat destruct (_ !! _); simplify_eq/=; by f_equal.
+  - apply (f_equal (.!! s)) in H. rewrite !lookup_fmap in H.
+    repeat destruct (_ !! _); simplify_eq/=; by f_equal.
+  - rewrite !fmap_delete. congruence.
+  - assert (∀ y, is_Some (ts !! y) ↔ is_Some (ts0 !! y)) as Hx.
+    { intros y. rewrite -!(fmap_is_Some (AttrN ∘ thunk_to_expr)) -!lookup_fmap.
+      by rewrite H. }
+    apply (map_minimal_key_Some _) in H5 as [[t1 Hx1] ?], H8 as [[t2 Hx2] ?].
+    assert (s0 = s) as -> by (apply (anti_symm attr_le); naive_solver).
+    pose proof (f_equal (.!! s) H) as Hs. rewrite !lookup_fmap in Hs.
+    rewrite !fmap_insert !fmap_empty /= !lookup_total_alt Hx1 Hx2 /=.
+    rewrite Hx1 Hx2 /= in Hs. simplify_eq/=. rewrite Hs !fmap_delete H. done.
+  - apply map_minimal_key_None in H8 as ->.
+    rewrite fmap_empty in H. by apply fmap_empty_inv in H as ->.
+  - apply map_minimal_key_None in H5 as ->.
+    rewrite fmap_empty in H. by apply symmetry, fmap_empty_inv in H as ->.
+Qed.
+
+Lemma interp_match_proper E1 E2 ts1 ts2 ms1 ms2 strict :
+  thunk_to_expr <$> ts1 = thunk_to_expr <$> ts2 →
+  fmap (M:=option) (subst_env E1) <$> ms1 = fmap (subst_env E2) <$> ms2 →
+  fmap (M:=gmap string) (tattr_to_attr E1) <$> interp_match ts1 ms1 strict
+  = fmap (tattr_to_attr E2) <$> interp_match ts2 ms2 strict.
+Proof.
+  revert ms2 ts1 ts2.
+  induction ms1 as [|x m1 ms1 Hmsx IH] using map_ind; intros ms2 ts1 ts2 Hts Hms.
+  { rewrite fmap_empty in Hms. apply symmetry, fmap_empty_inv in Hms as ->.
+    rewrite /interp_match !merge_empty_r. revert ts2 Hts.
+    induction ts1 as [|x t1 ts1 Htsx IH] using map_ind; intros ts2 Hts.
+    { rewrite fmap_empty in Hts. by apply symmetry, fmap_empty_inv in Hts as ->. }
+    rewrite fmap_insert in Hts.
+    apply symmetry, fmap_insert_inv in Hts as (t2&ts2'&?&Htsx2&->&Hts);
+      last by rewrite lookup_fmap Htsx.
+    rewrite !omap_insert /=. destruct strict; simpl;
+      rewrite ?map_mapM_insert_option ?delete_notin //= ?lookup_omap ?Htsx ?Htsx2;
+      auto. }
+  rewrite fmap_insert in Hms.
+  apply symmetry, fmap_insert_inv in Hms as (m2&ms2'&?&Hmsx2&->&Hms);
+    last by rewrite lookup_fmap Hmsx.
+  pose proof (f_equal (.!! x) Hts) as Hx. rewrite !lookup_fmap in Hx.
+  destruct (ts1 !! x) as [t1|] eqn:Hts1x, (ts2 !! x) as [t2|] eqn:Hts2x; simplify_eq/=.
+  - rewrite -(insert_delete ts1 x t1) // -(insert_delete ts2 x t2) //.
+    rewrite /interp_match. erewrite <-!insert_merge by done.
+    rewrite !map_mapM_insert_option ?lookup_merge ?lookup_delete ?Hmsx ?Hmsx2 //=.
+    apply (f_equal (delete x)) in Hts. rewrite -!fmap_delete in Hts.
+    eapply IH in Hms; [|done]. rewrite /interp_match in Hms.
+    repeat destruct (map_mapM id _); simplify_eq/=; [|done..].
+    rewrite !fmap_insert /=. auto with f_equal.
+  - rewrite /interp_match.
+    rewrite -!(insert_merge_r _ ts1 _ _ (inl <$> m1));
+      last (rewrite Hts1x; by destruct m1).
+    rewrite -!(insert_merge_r _ ts2 _ _ (inl <$> m2));
+      last (rewrite Hts2x; by destruct m2).
+    rewrite !map_mapM_insert_option ?lookup_merge ?Hts1x ?Hts2x ?Hmsx ?Hmsx2 //.
+    eapply IH in Hms; [|done]. rewrite /interp_match in Hms.
+    destruct m1, m2; simplify_eq/=; auto.
+    repeat destruct (map_mapM id _); simplify_eq/=; [|done..].
+    rewrite !fmap_insert /=. auto with f_equal.
+Qed.
+
+Lemma mapM_interp_proper' n ts1 ts2 mvs :
+  (∀ v1 v2 mv,
+    val_to_expr v1 = val_to_expr v2 →
+    force_deep n v1 = Res mv →
+    ∃ mw m, force_deep m v2 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw) →
+  (∀ t1 t2 mv,
+    thunk_to_expr t1 = thunk_to_expr t2 →
+    interp_thunk n t1 = Res mv →
+    ∃ mw m, interp_thunk m t2 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw) →
+  thunk_to_expr <$> ts1 = thunk_to_expr <$> ts2 →
+  mapM (mbind (force_deep n) ∘ interp_thunk n) ts1 = Res mvs →
+  ∃ mws m, mapM (mbind (force_deep m) ∘ interp_thunk m) ts2 = Res mws ∧
+           fmap (M:=list) val_to_expr <$> mvs = fmap (M:=list) val_to_expr <$> mws.
+Proof.
+  intros force_deep_proper interp_thunk_proper Hts.
+  revert mvs. rewrite list_eq_Forall2 Forall2_fmap in Hts.
+  induction Hts as [|t1 t2 ts1 ts2 ?? IH]; intros mvs ?; simplify_res.
+  { by exists (Some []), 0. }
+  destruct (interp_thunk _ _) as [mv|] eqn:Hinterp'; simplify_res.
+  eapply interp_thunk_proper in Hinterp'
+    as (mw & m1 & Hinterp1 & Hw); [|by eauto..].
+  destruct mv as [v|], mw as [w|]; simplify_res; last first.
+  { exists None, m1. by rewrite /= Hinterp1. }
+  destruct (force_deep _ _) as [mv'|] eqn:Hforce; simplify_res.
+  eapply force_deep_proper in Hforce as (mw' & m2 & Hforce2 & Hw'); last done.
+  destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+  { exists None, (m1 `max` m2).
+    rewrite (interp_thunk_le Hinterp1) /=; last lia.
+    rewrite (force_deep_le Hforce2) /=; last lia. done. }
+  destruct (mapM _ _) as [mvs'|] eqn:?; simplify_res.
+  destruct (IH _ eq_refl) as (mws & m3 & Hmap3 & ?).
+  exists ((w' ::.) <$> mws), (S (m1 `max` m2 `max` m3)).
+  rewrite (interp_thunk_le Hinterp1) /=; last lia.
+  rewrite (force_deep_le Hforce2) /=; last lia.
+  rewrite (mapM_interp_le Hmap3) /=; last lia. split; [by destruct mws|].
+  destruct mvs', mws; simplify_res; auto 10 with f_equal.
+Qed.
+
+Lemma force_deep_proper n v1 v2 mv :
+  val_to_expr v1 = val_to_expr v2 →
+  force_deep n v1 = Res mv →
+  ∃ mw m, force_deep m v2 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw
+with interp_proper n E1 E2 e1 e2 mv :
+  subst_env E1 e1 = subst_env E2 e2 →
+  interp n E1 e1 = Res mv →
+  ∃ mw m, interp m E2 e2 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw
+with interp_thunk_proper n t1 t2 mv :
+  thunk_to_expr t1 = thunk_to_expr t2 →
+  interp_thunk n t1 = Res mv →
+  ∃ mw m, interp_thunk m t2 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw
+with interp_app_proper n v1 v2 t1' t2' mv :
+  val_to_expr v1 = val_to_expr v2 →
+  thunk_to_expr t1' = thunk_to_expr t2' →
+  interp_app n v1 t1' = Res mv →
+  ∃ mw m, interp_app m v2 t2' = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  (* force_deep_proper *)
+  - destruct n as [|n]; [done|].
+    intros Hv Hinterp. rewrite force_deep_S /force_deep1 in Hinterp.
+    destruct v1 as [| | |ts1|ts1], v2 as [| | |ts2|ts2]; simplify_res.
+    { eexists _, 1; split; [by rewrite force_deep_S|]. done. }
+    { eexists _, 1; split; [by rewrite force_deep_S|]. simpl. auto with f_equal. }
+    { eexists _, 1; split; [by rewrite force_deep_S|]. simpl. auto with f_equal. }
+    { destruct (mapM _ _) as [mvs|] eqn:Hmap; simplify_res.
+      eapply mapM_interp_proper' in Hmap as (mws & m & Hmap & Hmvs); [|by eauto..].
+      exists (VList ∘ fmap Forced <$> mws), (S m).
+      rewrite force_deep_S /= Hmap. split; [done|].
+      destruct mvs, mws; simplify_eq/=; do 2 f_equal.
+      rewrite list_eq_Forall2 Forall2_fmap in Hmvs.
+      by rewrite list_eq_Forall2 !Forall2_fmap. }
+    destruct (map_mapM_sorted _ _ _) as [mvs|] eqn:Hmap; simplify_res.
+    assert (∃ mws m,
+      map_mapM_sorted attr_le
+        (mbind (force_deep m) ∘ interp_thunk m) ts2 = Res mws ∧
+      fmap (M:=gmap _) val_to_expr <$> mvs = fmap (M:=gmap _) val_to_expr <$> mws)
+      as (mws & m & Hmap' & Hmvs); last first.
+    { exists (VAttr ∘ fmap Forced <$> mws), (S m).
+      rewrite force_deep_S /= Hmap'. split; [done|].
+      destruct mvs, mws; simplify_eq/=; do 2 f_equal.
+      apply map_eq=> x. rewrite !lookup_fmap.
+      apply (f_equal (.!! x)) in Hmvs. rewrite !lookup_fmap in Hmvs.
+      repeat destruct (_ !! x); simplify_res; auto with f_equal. }
+    revert ts2 mvs Hmap Hv. induction ts1 as [|x t1 ts1 Hx1 ? IH]
+      using (map_sorted_ind attr_le); intros ts2' mvs Hmap Hts.
+    { exists (Some ∅), 0. rewrite fmap_empty in Hts.
+      apply symmetry, fmap_empty_inv in Hts as ->.
+      rewrite map_mapM_sorted_empty in Hmap; simplify_res.
+      by rewrite map_mapM_sorted_empty. }
+    rewrite map_mapM_sorted_insert //= in Hmap. rewrite fmap_insert in Hts.
+    apply symmetry, fmap_insert_inv in Hts as (t2 & ts2 & Ht & ? & -> & Hts);
+      simplify_eq/=; last by rewrite lookup_fmap Hx1.
+    assert (∀ j, is_Some (ts2 !! j) → attr_le x j).
+    { intros j. rewrite -(fmap_is_Some (AttrN ∘ thunk_to_expr)).
+      rewrite -lookup_fmap -Hts lookup_fmap fmap_is_Some. auto. }
+    destruct (interp_thunk _ _) as [mv|] eqn:Hinterp'; simplify_res.
+    eapply interp_thunk_proper in Hinterp'
+      as (mw & m1 & Hinterp1 & Hw); [|by eauto..].
+    destruct mv as [v|], mw as [w|]; simplify_res; last first.
+    { exists None, m1. by rewrite map_mapM_sorted_insert //= Hinterp1. }
+    destruct (force_deep _ _) as [mv'|] eqn:Hforce; simplify_res.
+    eapply force_deep_proper in Hforce as (mw' & m2 & Hforce2 & Hw'); last done.
+    destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+    { exists None, (m1 `max` m2). rewrite map_mapM_sorted_insert //=.
+      rewrite (interp_thunk_le Hinterp1) /=; last lia.
+      rewrite (force_deep_le Hforce2) /=; last lia. done. }
+    destruct (map_mapM_sorted _ _ _) as [mvs'|] eqn:?; simplify_res.
+    eapply IH in Hts as (mws & m3 & Hmap3 & ?); last done.
+    exists (<[x:=w']> <$> mws), (S (m1 `max` m2 `max` m3)).
+    rewrite map_mapM_sorted_insert //=.
+    rewrite (interp_thunk_le Hinterp1) /=; last lia.
+    rewrite (force_deep_le Hforce2) /=; last lia.
+    rewrite (map_mapM_interp_le Hmap3) /=; last lia.
+    destruct mvs' as [vs'|], mws as [ws'|]; simplify_res; last done.
+    split; [done|]. rewrite !fmap_insert. auto 10 with f_equal.
+  (* interp_proper *)
+  - destruct n as [|n]; [done|]. intros Hsubst Hinterp.
+    rewrite 2!subst_env_eq in Hsubst.
+    rewrite interp_S in Hinterp. destruct e1, e2; simplify_res; try done.
+    + (* ELit *)
+      case_guard; simplify_res.
+      * eexists (Some (VLit _ ltac:(done))), 1. by rewrite interp_lit.
+      * exists None, 1. split; [|done]. rewrite interp_S /=. by case_guard.
+    + (* EId *)
+      assert (∀ (mke : option (kind * expr)) (E : env) x,
+        prod_map id thunk_to_expr <$>
+          union_kinded (E !! x) (prod_map id (Thunk ∅) <$> mke)
+        = union_kinded (prod_map id thunk_to_expr <$> E !! x) mke) as HE.
+      { intros mke' E x. destruct (E !! _) as [[[] ?]|], mke' as [[[] ?]|];
+          simplify_eq/=; rewrite ?subst_env_empty //. }
+      rewrite -!HE {HE} in H.
+      destruct (union_kinded (E1 !! _) _) as [[k1 t1]|],
+        (union_kinded (E2 !! _) _) as [[k2 t2]|] eqn:HE2; simplify_res; last first.
+      { exists None, (S n). rewrite interp_S /=. by rewrite HE2. }
+      eapply interp_thunk_proper
+        in Hinterp as (mw & m & Hinterp & ?); [|by eauto..].
+      exists mw, (S (n `max` m)). split; [|done]. rewrite interp_S /= HE2 /=.
+      eauto using interp_thunk_le with lia.
+    + (* EAbs *) eexists (Some (VClo _ _ _)), 1; split; [by rewrite interp_S|].
+      simpl. auto with f_equal.
+    + (* EAbsMatch *)
+      eexists (Some (VCloMatch _ _ _ _)), 1; split; [by rewrite interp_S|].
+      simpl. auto with f_equal.
+    + (* EApp *)
+      destruct (interp n _ e1_1) as [mv1|] eqn:Hinterp'; simplify_eq/=.
+      eapply interp_proper in Hinterp' as (mw1 & m1 & Hinterp1 & ?); last done.
+      destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+      { exists None, (S m1). by rewrite interp_S /= Hinterp1. }
+      destruct (interp_app n _ _) as [mv'|] eqn:Hinterp'; simplify_res.
+      eapply (interp_app_proper _ _ _ _ (Thunk _ _)) in Hinterp'
+        as (mw & m2 & Hinterp2 & ?); [|done..].
+      exists mw, (S (m1 `max` m2)). rewrite interp_S /=.
+      rewrite (interp_le Hinterp1) /=; last lia.
+      rewrite (interp_app_le Hinterp2) /=; last lia. done.
+    + (* ESeq *)
+      destruct (interp n _ e1_1) as [mv1|] eqn:Hinterp'; simplify_eq/=.
+      eapply interp_proper in Hinterp' as (mw1 & m1 & Hinterp1 & ?); last done.
+      destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+      { exists None, (S m1). by rewrite interp_S /= Hinterp1. }
+      destruct μ0; simplify_res.
+      { eapply interp_proper in Hinterp as (w2 & m2 & Hinterp2 & ?); last done.
+        exists w2, (S (m1 `max` m2)). rewrite interp_S /=.
+        rewrite (interp_le Hinterp1) /=; last lia.
+        rewrite (interp_le Hinterp2) /=; last lia. done. }
+      destruct (force_deep _ _) as [mv'|] eqn:Hforce; simplify_res.
+      eapply force_deep_proper in Hforce as (mw' & m2 & Hforce & ?); last done.
+      destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+      { exists None, (S (m1 `max` m2)). rewrite interp_S /=.
+        rewrite (interp_le Hinterp1) /=; last lia.
+        rewrite (force_deep_le Hforce) /=; last lia. done. }
+      eapply interp_proper in Hinterp as (w2 & m3 & Hinterp3 & ?); last done.
+      exists w2, (S (m1 `max` m2 `max` m3)). rewrite interp_S /=.
+      rewrite (interp_le Hinterp1) /=; last lia.
+      rewrite (force_deep_le Hforce) /=; last lia.
+      rewrite (interp_le Hinterp3) /=; last lia. done.
+    + (* EList *)
+      eexists (Some (VList _)), 1; rewrite interp_S /=; split; [done|].
+      do 2 f_equal. revert es0 Hsubst.
+      induction es; intros [] ?; simplify_eq/=; f_equal/=; auto.
+    + (* EAttr *)
+      eexists (Some (VAttr _)), 1; rewrite interp_S /=; split; [done|].
+      do 2 f_equal. apply map_eq=> x. rewrite !lookup_fmap.
+      pose proof (f_equal (.!! x) Hsubst) as Hx. rewrite !lookup_fmap in Hx.
+      destruct (αs !! x) as [[[]]|], (αs0 !! x) as [[[]]|];
+        simplify_eq/=; do 2 f_equal; auto.
+      apply indirects_env_proper, Hx. by rewrite !tattr_to_attr_from_attr.
+    + (* ELetAttr *)
+      destruct (interp n _ _) as [mv'|] eqn:Hinterp'; simplify_eq/=.
+      eapply interp_proper in Hinterp' as (mw' & m1 & Hinterp1 & ?); last done.
+      destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+      { exists None, (S m1). by rewrite interp_S /= Hinterp1. }
+      destruct (maybe VAttr _) eqn:Hattr; simplify_res; last first.
+      { exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
+        by assert (maybe VAttr w' = None) as -> by (by destruct v', w'). }
+      destruct v', w'; simplify_res.
+      eapply interp_proper in Hinterp as (mw & m2 & Hinterp2 & ?);
+        [|by apply subst_env_union_fmap_proper].
+      exists mw, (S (m1 `max` m2)). rewrite interp_S /=.
+      rewrite (interp_le Hinterp1) /=; last lia.
+      rewrite (interp_le Hinterp2) /=; last lia. done.
+    + (* EBinOp *)
+      destruct (interp n _ e1_1) as [mv1|] eqn:Hinterp1; simplify_res.
+      eapply interp_proper in Hinterp1 as (mw1 & m1 & Hinterp1 & Hw1); last done.
+      destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+      { exists None. exists (S m1). by rewrite interp_S /= Hinterp1. }
+      apply (interp_bin_op_proper op0) in Hw1.
+      destruct (interp_bin_op _ v1) as [f|] eqn:Hop1,
+        (interp_bin_op _ w1) as [g|] eqn:Hop2; simplify_res; try done; last first.
+      { exists None. exists (S m1). by rewrite interp_S /= Hinterp1 /= Hop2. }
+      destruct (interp n _ e1_2) as [mv2|] eqn:Hinterp2; simplify_res.
+      eapply interp_proper in Hinterp2 as (mw2 & m2 & Hinterp2 & Hw2); last done.
+      destruct mv2 as [v2|], mw2 as [w2|]; simplify_res; last first.
+      { exists None. exists (S (m1 `max` m2)). rewrite interp_S /=.
+        rewrite (interp_le Hinterp1) /=; last lia.
+        rewrite Hop2 /= (interp_le Hinterp2) /=; last lia. done. }
+      apply Hw1 in Hw2.
+      destruct (f v2) as [t|] eqn:Hf,
+        (g w2) as [t'|] eqn:Hg; simplify_res; last first.
+      { exists None. exists (S (m1 `max` m2)). rewrite interp_S /=.
+        rewrite (interp_le Hinterp1) /=; last lia.
+        rewrite Hop2 /= (interp_le Hinterp2) /=; last lia. by rewrite Hg. }
+      eapply interp_thunk_proper in Hinterp
+        as (mw & m3 & Hforce3 & Hw); [|by eauto..].
+      exists mw, (S (m1 `max` m2 `max` m3)). rewrite interp_S /=. split; [|done].
+      rewrite (interp_le Hinterp1) /=; last lia.
+      rewrite Hop2 /= (interp_le Hinterp2) /=; last lia.
+      rewrite Hg /=. eauto using interp_thunk_le with lia.
+    + (* EIf *)
+      destruct (interp n _ e1_1) as [mv1|] eqn:Hinterp1; simplify_res.
+      eapply interp_proper in Hinterp1 as (mw1 & m1 & Hinterp1 & Hw1); last done.
+      destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+      { exists None. exists (S m1). by rewrite interp_S /= Hinterp1. }
+      destruct (maybe_VLit _ ≫= maybe LitBool) as [b|] eqn:Hbool;
+        simplify_res; last first.
+      { exists None. exists (S m1). rewrite interp_S /= Hinterp1 /=.
+        destruct v1, w1; repeat destruct select base_lit; naive_solver. }
+      eapply (interp_proper _ _ _ _ (if b then _ else _)) in Hinterp
+        as (mw & m2 & Hinterp & Hw); last by destruct b.
+      exists mw, (S (m1 `max` m2)). split; [|done]. rewrite interp_S /=.
+      rewrite (interp_le Hinterp1) /=; last lia.
+      assert (maybe_VLit w1 ≫= maybe LitBool = Some b) as ->.
+      { destruct v1, w1; repeat destruct select base_lit; naive_solver. }
+      rewrite /=. eauto using interp_le with lia.
+  (* interp_thunk_proper *)
+  - destruct n as [|n]; [done|].
+    intros Ht Hinterp. rewrite interp_thunk_S in Hinterp.
+    destruct t1 as [v1|E1 e1|x1 E1 tαs1], t2 as [v2|E2 e2|x2 E2 tαs2]; simplify_res.
+    + exists (Some v2), 1. rewrite interp_thunk_S /=. auto with f_equal.
+    + destruct (interp_val_to_expr E2 e2 v1) as (w & m & ? & ?); first done.
+      exists (Some w), (S m); simpl; auto with f_equal.
+    + by destruct v1.
+    + exists (Some v2), 1; split; [done|]; simpl.
+      symmetry. eauto using interp_val_to_expr_Res.
+    + eapply interp_proper in Hinterp as (mw & m & ? & ?); eauto.
+      exists mw, (S m). eauto.
+    + assert (∃ αs1, e1 = ESelect (EAttr αs1) x2 ∧
+        attr_subst_env E1 <$> αs1 = tattr_to_attr E2 <$> tαs2) as (αs1 & -> & Hαs).
+      { repeat match goal with
+        | H : subst_env _ ?e = _ |- _ =>
+            rewrite subst_env_eq in H; destruct e; simplify_eq; []
+        end; eauto. }
+      clear Ht. destruct n as [|n]; [done|].
+      rewrite !interp_S /= in Hinterp.
+      (* without [in Hinterp at 2 3] the termination checker loops *)
+      destruct n as [|n'] in Hinterp at 2 3; [done|].
+      rewrite !interp_S /= lookup_fmap in Hinterp.
+      pose proof (f_equal (.!! x2) Hαs) as Hx. rewrite !lookup_fmap in Hx.
+      destruct (αs1 !! x2) as [[[] e1]|],
+        (tαs2 !! x2) as [[e2|t2]|] eqn:Hx2; simplify_res.
+      * rewrite -tattr_to_attr_from_attr in Hαs.
+        destruct n as [|n]; [done|]. rewrite interp_thunk_S in Hinterp.
+        eapply interp_proper in Hinterp as (mw & m & Hinterp & ?);
+          last by apply indirects_env_proper.
+        exists mw, (S m). by rewrite interp_thunk_S /= Hx2.
+      * eapply interp_thunk_proper in Hinterp
+          as (mw & m & Hinterp & ?); last done.
+        exists mw, (S m). rewrite interp_thunk_S /= Hx2. done.
+      * exists None, (S n). by rewrite interp_thunk_S /= Hx2.
+    + by destruct v2.
+    + assert (∃ αs2, e2 = ESelect (EAttr αs2) x1 ∧
+        attr_subst_env E2 <$> αs2 = tattr_to_attr E1 <$> tαs1) as (αs2 & -> & Hαs).
+      { repeat match goal with
+        | H : _ = subst_env _ ?e |- _ =>
+            rewrite subst_env_eq in H; destruct e; simplify_eq; []
+        end; eauto. }
+      clear Ht.
+      pose proof (f_equal (.!! x1) Hαs) as Hx. rewrite !lookup_fmap in Hx.
+      destruct (tαs1 !! x1) as [[e1|t1]|],
+        (αs2 !! x1) as [[[] e2]|] eqn:Hx2; simplify_res.
+      * rewrite -tattr_to_attr_from_attr in Hαs.
+        eapply interp_proper in Hinterp as (mw & m & Hinterp & ?);
+          last by apply indirects_env_proper.
+        exists mw, (S (S (S m))). rewrite interp_thunk_S /= !interp_S /=.
+        rewrite lookup_fmap Hx2 /= interp_thunk_S /=. done.
+      * apply (interp_thunk_proper _ _ (Thunk E2 e2))
+          in Hinterp as (mw & m & Hinterp & ?); last done.
+        destruct m as [|m]; [done|].
+        exists mw, (S (S (S m))). rewrite interp_thunk_S /= !interp_S /=.
+        rewrite lookup_fmap Hx2 /= interp_thunk_S /=. done.
+      * exists None, (S (S (S n))). rewrite interp_thunk_S /= !interp_S /=.
+        rewrite lookup_fmap Hx2 /=. done.
+    + pose proof (f_equal (.!! x2) Ht) as Hx. rewrite !lookup_fmap in Hx.
+      destruct (tαs1 !! x2) as [[e1|t1]|] eqn:Hx1,
+        (tαs2 !! _) as [[e2|t2]|] eqn:Hx2; simplify_res.
+      * eapply interp_proper in Hinterp
+          as (mw & m & Hinterp & ?); [|by apply indirects_env_proper].
+        exists mw, (S m). rewrite interp_thunk_S /= Hx2. done. 
+      * eapply interp_thunk_proper in Hinterp as (mw & m & Hinterp & ?); [|done].
+        exists mw, (S m). rewrite interp_thunk_S /= Hx2. done.
+      * exists None, 1. by rewrite interp_thunk_S /= Hx2.
+  (* interp_app_proper *)
+  - destruct n as [|n]; [done|].
+    intros Hv Ht Hinterp. rewrite interp_app_S /= in Hinterp.
+    destruct v1, v2; simplify_res.
+    + (* VLit *) by eexists None, 1.
+    + (* VClo *)
+      eapply interp_proper in Hinterp as (mw & m & Hinterp' & ?);
+        last by eapply subst_env_insert_proper.
+      eexists _, (S m). rewrite interp_app_S /= Hinterp'. done.
+    + (* VCloMatch *)
+      destruct (interp_thunk n t1') as [mv1|] eqn:Hthunk; simplify_res.
+      eapply interp_thunk_proper in Hthunk as (mw1 & m1 & Hthunk & Hw); [|by eauto..].
+      destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+      { exists None, (S m1). split; [|done].
+        rewrite interp_app_S /= Hthunk /=. done. }
+      destruct (maybe VAttr v1) as [ts1|] eqn:?; simplify_res; last first.
+      { exists None, (S m1). split; [|done].
+        rewrite interp_app_S /= Hthunk /=. destruct v1, w1; naive_solver. }
+      destruct v1, w1; simplify_eq/=.
+      rewrite 2!map_fmap_compose in Hw. apply (inj _) in Hw.
+      eapply (interp_match_proper _ _ _ _ _ _ strict0) in Hw; last done.
+      destruct (interp_match ts1 _ _) as [tαs1|] eqn:Hmatch1,
+        (interp_match ts0 _ _) as [tαs2|] eqn:Hmatch2;
+        simplify_res; try done; last first.
+      { exists None, (S m1). split; [|done].
+        rewrite interp_app_S /= Hthunk /= Hmatch2. done. }
+      eapply interp_proper in Hinterp as (mw & m2 & Hinterp & ?); last first.
+      { by apply indirects_env_proper. }
+      exists mw, (S (m1 `max` m2)). split; [|done].
+      rewrite interp_app_S /=.
+      rewrite (interp_thunk_le Hthunk) /=; last lia.
+      rewrite Hmatch2 /=. eauto using interp_le with lia.
+    + (* VList *) by eexists None, 1.
+    + (* VAttr *)
+      pose proof (f_equal (.!! "__functor") Hv) as Htf.
+      rewrite !lookup_fmap /= in Htf.
+      destruct (ts !! _) as [e|] eqn:Hfunc, (ts0 !! _) as [e'|] eqn:Hfunc';
+        simplify_res; last first.
+      { exists None, 1. by rewrite interp_app_S /= Hfunc'. }
+      destruct (interp_thunk _ _) as [mv'|] eqn:Hinterp'; simplify_res.
+      eapply interp_thunk_proper in Hinterp'
+        as (mw' & m1 & Hinterp1 & Hw'); [|by eauto..].
+      destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+      { exists None, (S m1). by rewrite interp_app_S /= Hfunc' /= Hinterp1. }
+      destruct (interp_app _ _ _) as [mv'|] eqn:Happ; simplify_res.
+      eapply (interp_app_proper _ _ _ _ (Forced (VAttr _))) in Happ
+        as (mw' & m2 & Happ2 & ?); [|done|by rewrite /= Hv].
+      destruct mv', mw'; simplify_res; last first.
+      { exists None, (S (m1 `max` m2)). rewrite interp_app_S /= Hfunc' /=.
+        rewrite (interp_thunk_le Hinterp1) /=; last lia.
+        rewrite (interp_app_le Happ2) /=; last lia. done. }
+      eapply interp_app_proper in Hinterp as (mw' & m3 & Happ3 & ?); [|done..].
+      exists mw', (S (m1 `max` m2 `max` m3)). rewrite interp_app_S /= Hfunc' /=.
+      rewrite (interp_thunk_le Hinterp1) /=; last lia.
+      rewrite (interp_app_le Happ2) /=; last lia.
+      rewrite (interp_app_le Happ3) /=; last lia. done.
+Qed.
+
+Lemma mapM_interp_proper n ts1 ts2 mvs :
+  thunk_to_expr <$> ts1 = thunk_to_expr <$> ts2 →
+  mapM (mbind (force_deep n) ∘ interp_thunk n) ts1 = Res mvs →
+  ∃ mws m, mapM (mbind (force_deep m) ∘ interp_thunk m) ts2 = Res mws ∧
+           fmap (M:=list) val_to_expr <$> mvs = fmap (M:=list) val_to_expr <$> mws.
+Proof. eauto using mapM_interp_proper', force_deep_proper, interp_thunk_proper. Qed.
+
+Lemma interp_thunk_as_interp n t mv :
+  interp_thunk n t = Res mv →
+  ∃ mw m, interp m ∅ (thunk_to_expr t) = Res mw ∧
+          val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  revert t mv. induction n as [|n IH]; intros t mv Hinterp; [done|].
+  rewrite interp_thunk_S in Hinterp. destruct t as [v|E e|x E tαs]; simplify_res.
+  { destruct (interp_empty_val_to_expr v) as (w & m & Hinterp & ?).
+    exists (Some w), m; simpl; auto using f_equal. }
+  { eapply interp_proper, Hinterp. by rewrite subst_env_empty. }
+  destruct (tαs !! x) as [[e|t]|] eqn:Hx; simplify_res.
+  - eapply interp_proper in Hinterp as (mw & m & Hinterp & ?);
+      last apply subst_env_indirects_env.
+    exists mw, (S (S m)). rewrite !interp_S /=.
+    rewrite !lookup_fmap Hx /= interp_thunk_S /=. done.
+  - apply IH in Hinterp as (mw & m & Hinterp & ?).
+    exists mw, (S (S m)). rewrite !interp_S /=.
+    rewrite !lookup_fmap Hx /= interp_thunk_S //=.
+  - exists None, (S (S n)). rewrite !interp_S /=.
+    by rewrite !lookup_fmap Hx /=.
+Qed.
+
+Lemma interp_as_interp_thunk n t mv :
+  interp n ∅ (thunk_to_expr t) = Res mv →
+  ∃ mw m, interp_thunk m t = Res mw ∧
+          val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  revert t mv. induction (lt_wf n) as [[|n] _ IH]; intros t mv Hinterp; [done|].
+  destruct t as [v|E e|x E tαs]; simplify_res.
+  { apply interp_empty_val_to_expr_Res in Hinterp. by exists (Some v), 1. }
+  { eapply (interp_proper _ _ E) in Hinterp as (mw & m & Hinterp & ?);
+      [|by rewrite subst_env_empty].
+    exists mw, (S m). by rewrite interp_thunk_S /=. }
+  destruct n as [|n]; [done|]. rewrite !interp_S /= in Hinterp.
+  rewrite !lookup_fmap in Hinterp.
+  destruct (tαs !! x) as [[e|t]|] eqn:Hx; simplify_res.
+  - rewrite interp_thunk_S /= in Hinterp.
+    eapply interp_proper in Hinterp as (mw & m & Hinterp & ?);
+      last apply symmetry, subst_env_indirects_env.
+    exists mw, (S m). rewrite interp_thunk_S /= Hx. done.
+  - rewrite interp_thunk_S /= in Hinterp.
+    eapply IH in Hinterp as (mw & m & Hinterp & ?); last lia.
+    exists mw, (S m). rewrite !interp_thunk_S /= Hx. done.
+  - exists None, (S n). rewrite !interp_thunk_S /= Hx. done.
+Qed.
+
+Lemma delayed_interp n e e' mv :
+  interp n ∅ e' = Res mv →
+  e =D=> e' →
+  ∃ m, interp m ∅ e = Res mv.
+Proof.
+  intros Hinterp Hdel. revert n mv Hinterp. induction Hdel; intros n mv Hinterp.
+  - by eauto.
+  - apply IHHdel in Hinterp as [m Hinterp].
+    exists (S (S m)). rewrite interp_S /= lookup_empty left_id_L /=.
+    by rewrite interp_thunk_S /=.
+  - destruct n as [|n]; [done|]. rewrite interp_S /= in Hinterp.
+    destruct (interp _ _ e1') as [mv1|] eqn:Hinterp1; simplify_res.
+    apply IHHdel1 in Hinterp1 as [m1 Hinterp1].
+    destruct mv1 as [v1|]; simplify_res; last first.
+    { exists (S m1). by rewrite interp_S /= Hinterp1. }
+    destruct (interp_bin_op op v1) as [f|] eqn:Hf; simplify_res; last first.
+    { exists (S m1). by rewrite interp_S /= Hinterp1 /= Hf. }
+    destruct (interp _ _ e2') as [mv2|] eqn:Hinterp2; simplify_res.
+    apply IHHdel2 in Hinterp2 as [m2 Hinterp2]. exists (S (n `max` m1 `max` m2)).
+    rewrite interp_S /= (interp_le Hinterp1); last lia.
+    rewrite /= Hf /= (interp_le Hinterp2); last lia.
+    destruct mv2; simplify_res; [|done].
+    destruct (f _); simplify_res; [|done].
+    eauto using interp_thunk_le with lia.
+  - destruct n as [|n]; [done|]. rewrite interp_S /= in Hinterp.
+    destruct (interp _ _ e1') as [mv1|] eqn:Hinterp1; simplify_res.
+    apply IHHdel1 in Hinterp1 as [m1 Hinterp1].
+    destruct mv1 as [v1|]; simplify_res; last first.
+    { exists (S m1). by rewrite interp_S /= Hinterp1. }
+    destruct (maybe_VLit v1 ≫= maybe LitBool) as [[]|] eqn: Hbool; simplify_res.
+    + apply IHHdel2 in Hinterp as [m2 Hinterp2]. exists (S (m1 `max` m2)).
+      rewrite interp_S /= (interp_le Hinterp1); last lia.
+      rewrite /= Hbool /=. eauto using interp_le with lia.
+    + apply IHHdel3 in Hinterp as [m3 Hinterp3]. exists (S (m1 `max` m3)).
+      rewrite interp_S /= (interp_le Hinterp1); last lia.
+      rewrite /= Hbool /=. eauto using interp_le with lia.
+    + exists (S m1). rewrite interp_S /= Hinterp1 /= Hbool. done.
+Qed.
+
+Lemma interp_subst_abs n x e1 e2 mv :
+  interp n ∅ (subst {[x:=(ABS, e2)]} e1) = Res mv →
+  ∃ mw m, interp m (<[x:=(ABS, Thunk ∅ e2)]> ∅) e1 = Res mw ∧
+          val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  apply interp_proper. by rewrite subst_env_empty subst_abs_as_subst_env.
+Qed.
+
+Lemma interp_subst_indirects n e αs mv :
+  interp n ∅ (subst (indirects αs) e) = Res mv →
+  ∃ mw m,
+    interp m (indirects_env ∅ (attr_to_tattr ∅ <$> αs)) e = Res mw ∧
+    val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  apply interp_proper. rewrite subst_env_empty. rewrite subst_env_alt.
+  f_equal. apply map_eq=> x. rewrite !lookup_fmap.
+  destruct (αs !! x) eqn:?; do 2 f_equal/=;
+    rewrite /indirects /indirects_env right_id_L !map_lookup_imap
+      !lookup_fmap !Heqo //=.
+  rewrite tattr_to_attr_from_attr_empty //.
+Qed.
+
+Lemma interp_subst_fmap k n e es mv :
+  interp n ∅ (subst ((k,.) <$> es) e) = Res mv →
+  ∃ mw m, interp m ((k,.) ∘ Thunk ∅ <$> es) e = Res mw ∧
+          val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  apply interp_proper. rewrite subst_env_empty. rewrite subst_env_alt.
+  f_equal. apply map_eq=> x. rewrite !lookup_fmap.
+  destruct (es !! x) as [d|]; do 2 f_equal/=. by rewrite subst_env_empty.
+Qed.
+
+Lemma final_interp μ e :
+  final μ e →
+  ∃ w m, interp m ∅ e = mret w ∧ e = val_to_expr w.
+Proof.
+  revert μ. induction e; intros μ'; intros Hfinal; try by inv Hfinal.
+  - inv Hfinal. eexists (VLit _ _), 1. by rewrite interp_lit /=.
+  - eexists (VClo _ _ _), 1. rewrite interp_S /=. split; [done|].
+    by rewrite /= subst_env_empty.
+  - eexists (VCloMatch _ _ _ _), 1. rewrite interp_S /=. split; [done|].
+    rewrite /= subst_env_empty. f_equal.
+    apply map_eq=> x. rewrite lookup_fmap.
+    destruct (ms !! x) as [[]|]; do 2 f_equal/=. by rewrite subst_env_empty.
+  - eexists (VList _), 1. rewrite interp_S /=. split; [done|]. f_equal. clear.
+    induction es; f_equal/=; [|done].
+    by rewrite /= subst_env_empty.
+  - eexists (VAttr _), 1. rewrite interp_S /=. split; [done|].
+    f_equal. apply map_eq=> x.
+    assert (no_recs αs) by (by inv Hfinal).
+    rewrite from_attr_no_recs // !lookup_fmap.
+    destruct (_ !! _) as [[]|] eqn:?; f_equal/=.
+    f_equal; eauto using no_recs_lookup, subst_env_empty.
+Qed.
+
+Lemma final_force_deep' v :
+  final DEEP (val_to_expr v) →
+  ∃ w m, force_deep m v = mret w ∧ val_to_expr v = val_to_expr w.
+Proof.
+  intros Hfinal. remember (val_to_expr v) as e eqn:He.
+  revert v He. induction e; intros [] ?; simplify_eq/=; inv Hfinal.
+  - (* VLit *) eexists (VLit _ _), 1. by rewrite force_deep_S.
+  - (* VClo *)
+    eexists (VClo _ _ _), 1. by rewrite force_deep_S.
+  - (* VCloMatch *)
+    eexists (VCloMatch _ _ _ _), 1. by rewrite force_deep_S.
+  - (* VList *)
+    assert (∃ vs m, mapM (mbind (force_deep m) ∘ interp_thunk m) ts = mret vs ∧
+      val_to_expr <$> vs = thunk_to_expr <$> ts)
+      as (vs & m & Hmap & Hvs); last first.
+    { exists (VList (Forced <$> vs)), (S m). rewrite force_deep_S /= Hmap /=.
+      split; [done|]. f_equal. rewrite -Hvs.
+      clear. by induction vs; by f_equal/=. }
+    rewrite Forall_fmap in H1. induction H1 as [|t ts Ht ? IH]; simplify_eq/=.
+    { by exists [], 0. }
+    apply Forall_cons in H as [IHt IHts].
+    destruct IH as (ws & m1 & Hinterp1 & ?); simplify_eq/=; [done|]. clear IHts.
+    destruct (final_interp DEEP (thunk_to_expr t))
+      as (v' & m & Hinterp & ?); [done|].
+    apply interp_as_interp_thunk in Hinterp
+      as ([v''|] & m' & Hinterp & ?); simplify_res.
+    destruct (IHt Ht v'') as (w & m'' & Hforce & ?); [congruence|].
+    exists (w :: ws), (m1 `max` m' `max` m''); csimpl.
+    rewrite (interp_thunk_le Hinterp) /=; last lia.
+    rewrite (force_deep_le Hforce) /=; last lia.
+    rewrite (mapM_interp_le Hinterp1) /=; last lia. auto with f_equal.
+  - (* VAttr *) clear H1. assert (∃ vs m,
+      map_mapM_sorted attr_le
+        (mbind (force_deep m) ∘ interp_thunk m) ts = mret vs ∧
+      val_to_expr <$> vs = thunk_to_expr <$> ts)
+      as (vs & m & Hmap & Hvs); last first.
+    { exists (VAttr (Forced <$> vs)), (S m). rewrite force_deep_S /= Hmap /=.
+      split; [done|]. rewrite 2!map_fmap_compose -Hvs. f_equal.
+      apply map_eq=> x. rewrite !lookup_fmap. by destruct (vs !! x). }
+    induction ts as [|x t ts Hx ? IH] using (map_sorted_ind attr_le).
+    { exists ∅, 0. by rewrite map_mapM_sorted_empty. }
+    rewrite fmap_insert /= in H, H2.
+    apply map_Forall_insert in H as [IHt IHts]; last by rewrite lookup_fmap Hx.
+    apply map_Forall_insert in H2 as [Ht Hts]; last by rewrite lookup_fmap Hx.
+    apply IH in IHts as (ws & m1 & Hinterp1 & ?); clear IH; simplify_eq/=; last done.
+    destruct (final_interp DEEP (thunk_to_expr t))
+      as (v' & m & Hinterp & ?); [done|].
+    apply interp_as_interp_thunk in Hinterp
+      as ([v''|] & m' & Hinterp & ?); simplify_res.
+    destruct (IHt Ht v'') as (w & m'' & Hforce & ?); [congruence|].
+    exists (<[x:=w]> ws), (m1 `max` m' `max` m'').
+    rewrite fmap_insert map_mapM_sorted_insert //=.
+    rewrite (interp_thunk_le Hinterp) /=; last lia.
+    rewrite (force_deep_le Hforce) /=; last lia.
+    rewrite (map_mapM_interp_le Hinterp1) /=; last lia.
+    rewrite fmap_insert. auto with f_equal.
+Qed.
+
+Lemma interp_step μ e1 e2 :
+  e1 -{μ}-> e2 →
+  (∀ n mv,
+     ¬final SHALLOW e1 →
+     interp n ∅ e2 = Res mv →
+     exists mw m, interp m ∅ e1 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw) ∧
+  (∀ n v1 v2 mv,
+     μ = DEEP →
+     e1 = val_to_expr v1 →
+     e2 = val_to_expr v2 →
+     force_deep n v2 = Res mv →
+     exists mw m, force_deep m v1 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw).
+Proof.
+  intros Hstep. induction Hstep; inv_step.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    apply interp_subst_abs in Hinterp as (mw & [|m] & Hinterp & Hv); simplify_eq/=.
+    exists mw, (S (S (S m))). split; [|done].
+    rewrite interp_S /= interp_app_S /= /= !interp_S /=.
+    rewrite -!interp_S /=. rewrite (interp_le Hinterp); last lia. done.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct n as [|n]; simplify_eq/=. apply interp_match_Some_2 in H0.
+    apply interp_subst_indirects in Hinterp as (mw & m & Hinterp & ?).
+    exists mw, (S (S (S (S m)))); split; [|done].
+    rewrite !interp_S /= interp_app_S /= interp_thunk_S /= (interp_S m) /=.
+    rewrite from_attr_no_recs // map_fmap_compose H0 /=.
+    eauto using interp_le with lia.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct n as [|[|[|n]]]; simplify_eq/=.
+    rewrite !interp_S /= -!interp_S in Hinterp.
+    destruct (interp _ _ e1) as [mw|] eqn:Hinterp'; simplify_res.
+    destruct mw as [w|]; simplify_res; last first.
+    { exists None, (S (S (S (S n)))). split; [|done].
+      rewrite 2!interp_S /= interp_app_S /=.
+      rewrite from_attr_no_recs // lookup_fmap H0 /=.
+      rewrite interp_thunk_S /= Hinterp'. done. }
+    destruct (interp_app _ _ _) as [mv'|] eqn:Happ; simplify_res.
+    eapply (interp_app_proper _ _ _ _
+      (Forced (VAttr (Thunk ∅ ∘ attr_expr <$> αs))))
+      in Happ as (mw' & m1 & Happ1 & Hw); [|done|]; last first.
+    { rewrite /= subst_env_eq /=. f_equal.
+      apply map_eq=> y. rewrite !lookup_fmap.
+      destruct (αs !! y) as [[]|] eqn:?; do 2 f_equal/=; eauto using no_recs_lookup. }
+    destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+    { exists None, (S (S (S (S (n `max` m1))))). split; [|done].
+      rewrite 2!interp_S /= interp_app_S /=.
+      rewrite from_attr_no_recs // lookup_fmap H0 /=.
+      rewrite interp_thunk_S /= (interp_le Hinterp') /=; last lia.
+      rewrite (interp_app_le Happ1); last lia. done. }
+    eapply interp_app_proper in Hinterp as (mw & m2 & ? & Hinterp); [|done..].
+    exists mw, (S (S (S (S (n `max` m1 `max` m2))))). split; [|done].
+    rewrite !interp_S /= interp_app_S /=.
+    rewrite from_attr_no_recs // lookup_fmap H0 /=.
+    rewrite interp_thunk_S /= (interp_le Hinterp') /=; last lia.
+    rewrite (interp_app_le Happ1) /=; last lia.
+    eauto using interp_app_le with lia.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct (final_interp μ' e1) as (v & m & Hinterp' & ->); first done.
+    destruct μ'.
+    { exists mv, (S (n `max` m)). rewrite interp_S /=.
+      rewrite (interp_le Hinterp) /=; last lia.
+      by rewrite (interp_le Hinterp') /=; last lia. }
+    destruct (final_force_deep' v) as (w & m' & Hforce & ?); first done.
+    exists mv, (S (n `max` m `max` m')). rewrite interp_S /=.
+    rewrite (interp_le Hinterp) /=; last lia.
+    rewrite (interp_le Hinterp') /=; last lia.
+    by rewrite (force_deep_le Hforce) /=; last lia.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    rewrite map_fmap_compose in Hinterp.
+    apply interp_subst_fmap in Hinterp as (mw & [|m] & Hinterp & Hv); simplify_eq/=.
+    rewrite map_fmap_compose in Hinterp.
+    exists mw, (S (S m)). rewrite !interp_S /= -interp_S.
+    rewrite from_attr_no_recs // right_id_L map_fmap_compose. done.
+  - split; last first.
+    { intros n [] v2 mv _ Hαs; simplify_eq/=. by destruct H. }
+    intros n mv _ Hinterp. destruct n as [|n]; [done|].
+    rewrite interp_S /= in Hinterp; simplify_res.
+    eexists _, 1; split; [by rewrite interp_S|].
+    do 2 f_equal/=. apply map_eq=> x /=. rewrite !lookup_fmap.
+    destruct (αs !! x) as [[[] ?]|]; do 2 f_equal/=.
+    by rewrite subst_env_indirects_env_attr_to_tattr_empty subst_env_empty.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    apply final_interp in H as (v1 & m1 & Hinterp1 & ->).
+    pose proof H1 as Hsem. apply interp_bin_op_Some_2 in H1 as [f Hf].
+    eapply final_interp in H0 as (v2 & m2 & Hinterp2 & ->).
+    eapply interp_bin_op_Some_Some_2 in H2 as (t3 & Hfv & Hdel); [|done..].
+    eapply delayed_interp in Hinterp as (m3 & Hinterp); [|done].
+    apply interp_as_interp_thunk in Hinterp as (mw & m & Hinterp3 & ?).
+    exists mw, (S (m `max` m1 `max` m2)). split; [|done]. rewrite interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia.
+    rewrite Hf /= (interp_le Hinterp2) /=; last lia.
+    rewrite Hfv /= (interp_thunk_le Hinterp3); last lia. done.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    exists mv, (S (S n)). rewrite !interp_S /= -interp_S.
+    eauto using interp_le with lia.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    exists mv, (S (S n)). rewrite !interp_S /= lookup_empty /=. done.
+  - split; [intros ?? []; constructor; by eauto|].
+    intros n [] [] mv _ Hts Hts' Hforce; simplify_eq.
+    destruct n as [|n]; [done|rewrite force_deep_S /= in Hforce].
+    destruct (mapM _ _) as [mvs|] eqn:Hmap; simplify_eq/=.
+    destruct IHHstep as [IH1 IH2].
+    apply symmetry, fmap_app_inv in Hts
+      as (ts1 & [|t1 ts1'] & ? & ? & ?); simplify_eq/=.
+    apply symmetry, fmap_app_inv in Hts'
+      as (ts2 & [|t2 ts2'] & Hts & ? & ?); simplify_eq/=.
+    assert (∃ mws m,
+      mapM (mbind (force_deep m) ∘ interp_thunk m) (ts1 ++ t1 :: ts1') = Res mws ∧
+      fmap (M:=list) val_to_expr <$> mvs = fmap (M:=list) val_to_expr <$> mws)
+      as (mws & m & Hmap' & Hmvs); last first.
+    { exists (VList ∘ fmap Forced <$> mws), (S m). rewrite force_deep_S /= Hmap'.
+      split; [done|].
+      destruct mvs as [vs|], mws as [ws|]; simplify_eq/=; do 2 f_equal.
+      rewrite list_eq_Forall2 Forall2_fmap in Hmvs.
+      by rewrite list_eq_Forall2 !Forall2_fmap. }
+    rewrite mapM_res_app in Hmap.
+    destruct (mapM _ ts2) as [mvs1|] eqn:Hmap1; simplify_res.
+    eapply mapM_interp_proper in Hmap1 as (mws1 & m1 & Hmap1 & ?); [|done].
+    destruct mvs1 as [vs1|], mws1 as [ws1|]; simplify_res; last first.
+    { exists None, m1. by rewrite mapM_res_app Hmap1. }
+    destruct (interp_thunk n t2) as [mw|] eqn:Hinterp; simplify_res.
+    apply interp_thunk_as_interp in Hinterp as (mw' & m & Hinterp & Hmw').
+    destruct (default mfail (force_deep n <$> mw))
+      as [mu|] eqn:Hforce; simplify_res.
+    destruct (step_any_shallow  _ _ _ Hstep) as [|Hfinal1].
+    + (* SHALLOW *)
+      apply IH1 in Hinterp as (mw'' & m' & Hinterp & Hmw'');
+        [|by eauto using step_not_final].
+      apply interp_as_interp_thunk in Hinterp as (mw''' & m2 & Hinterp & ?).
+      destruct mw as [w|], mw', mw'', mw''' as [w'''|]; simplify_res; last first.
+      { exists None, (m1 `max` m2). rewrite mapM_res_app.
+        rewrite (mapM_interp_le Hmap1) /=; last lia.
+        rewrite (interp_thunk_le Hinterp) /=; last lia. done. }
+      eapply (force_deep_proper _ _ w''')
+        in Hforce as (mu' & m3 & Hforce & ?); last congruence.
+      destruct mu as [u|], mu' as [u'|]; simplify_res; last first.
+      { exists None, (m1 `max` m2 `max` m3). rewrite mapM_res_app.
+        rewrite (mapM_interp_le Hmap1) /=; last lia.
+        rewrite (interp_thunk_le Hinterp) /=; last lia.
+        rewrite (force_deep_le Hforce) /=; last lia. done. }
+      destruct (mapM _ ts2') as [mvs2|] eqn:Hmap2; simplify_res.
+      eapply mapM_interp_proper in Hmap2 as (mws2 & m4 & Hmap2 & ?); [|done].
+      exists ((ws1 ++.) ∘ (u' ::.) <$> mws2), (m1 `max` m2 `max` m3 `max` m4).
+      rewrite mapM_res_app.
+      rewrite (mapM_interp_le Hmap1) /=; last lia.
+      rewrite (interp_thunk_le Hinterp) /=; last lia.
+      rewrite (force_deep_le Hforce) /=; last lia.
+      rewrite (mapM_interp_le Hmap2) /=; last lia. split; [by destruct mws2|].
+      destruct mvs2, mws2; simplify_res; f_equal. rewrite !fmap_app !fmap_cons.
+      congruence.
+    + (* DEEP *)
+      apply step_final_shallow in Hstep as Hfinal2; last done.
+      apply final_interp in Hfinal1 as (w1 & m2 & Hinterpt1 & ?).
+      apply interp_as_interp_thunk in Hinterpt1 as (mw'' & m3 & Hinterpt1 & ?).
+      apply final_interp in Hfinal2 as (w2' & m4 & Hinterpt2 & ?).
+      eapply interp_agree in Hinterp; last apply Hinterpt2.
+      destruct mw as [w2|], mw'' as [w2''|]; simplify_res.
+      eapply IH2 in Hforce as (mu' & m5 & Hforce & ?); [|by auto with congruence..].
+      eapply (force_deep_proper _ _ w2'')
+        in Hforce as (mu'' & m6 & Hforce & ?); last congruence.
+      destruct mu as [u|], mu' as [u'|], mu'' as [u''|]; simplify_res; last first.
+      { exists None, (m1 `max` m3 `max` m6). rewrite mapM_res_app.
+        rewrite (mapM_interp_le Hmap1) /=; last lia.
+        rewrite (interp_thunk_le Hinterpt1) /=; last lia.
+        rewrite (force_deep_le Hforce) /=; last lia. done. }
+      destruct (mapM _ ts2') as [mvs2|] eqn:Hmap2; simplify_res.
+      eapply mapM_interp_proper in Hmap2 as (mws2 & m7 & Hmap2 & ?); [|done].
+      exists ((ws1 ++.) ∘ (u'' ::.) <$> mws2), (m1 `max` m3 `max` m6 `max` m7).
+      rewrite mapM_res_app.
+      rewrite (mapM_interp_le Hmap1) /=; last lia.
+      rewrite (interp_thunk_le Hinterpt1) /=; last lia.
+      rewrite (force_deep_le Hforce) /=; last lia.
+      rewrite (mapM_interp_le Hmap2) /=; last lia. split; [by destruct mws2|].
+      destruct mvs2, mws2; simplify_res; f_equal. rewrite !fmap_app !fmap_cons.
+      congruence.
+  - split; [intros ?? []; constructor; by eauto using no_recs_insert|].
+    intros n [] [] mv _ Hts Hts' Hforce; simplify_eq.
+    destruct n as [|n]; [done|rewrite force_deep_S /= in Hforce].
+    destruct (map_mapM_sorted _ _ _) as [mvs|] eqn:Hmap; simplify_eq/=.
+    destruct IHHstep as [IH1 IH2].
+    apply symmetry, fmap_insert_inv in Hts
+      as (t1 & ts1 & ? & Hx1 & ? & ?); simplify_eq/=; last done.
+    apply symmetry, fmap_insert_inv in Hts' as (t2 & ts2 & ? & Hx2 & ? & Hts);
+      simplify_eq/=; last by rewrite lookup_fmap Hx1.
+    assert (∃ mws m,
+      map_mapM_sorted attr_le (mbind (force_deep m) ∘ interp_thunk m)
+        (<[x:=t1]> ts1) = Res mws ∧
+      fmap (M:=gmap _) val_to_expr <$> mvs = fmap (M:=gmap _) val_to_expr <$> mws)
+      as (mws & m & Hmap' & Hmvs); last first.
+    { exists (VAttr ∘ fmap Forced <$> mws), (S m). rewrite force_deep_S /= Hmap'.
+      split; [done|].
+      destruct mvs as [vs|], mws as [ws|]; simplify_eq/=; do 2 f_equal.
+      apply map_eq=> y. rewrite !lookup_fmap.
+      apply (f_equal (.!! y)) in Hmvs. rewrite !lookup_fmap in Hmvs.
+      destruct (vs !! _), (ws !! _); simplify_eq/=; auto with f_equal. }
+    destruct (step_any_shallow  _ _ _ Hstep) as [|Hfinal].
+    + (* SHALLOW *) assert (map_Forall2 (λ _ t1 t2, ∀ n mv,
+        interp n ∅ (thunk_to_expr t2) = Res mv →
+        ∃ mw m, interp m ∅ (thunk_to_expr t1) = Res mw ∧
+          val_to_expr <$> mv = val_to_expr <$> mw)
+        (<[x:=t1]> ts1) (<[x:=t2]> ts2)) as IHts.
+      { apply map_Forall2_insert_2; first by eauto using step_not_final.
+        intros y. apply (f_equal (.!! y)) in Hts. rewrite !lookup_fmap in Hts.
+        destruct (ts1 !! y), (ts2 !! y); simplify_eq/=; constructor.
+        rewrite -Hts; eauto. }
+      revert IHts Hmap. generalize (<[x:=t1]> ts1) (<[x:=t2]> ts2). clear.
+      intros ts1. revert n mvs.
+      induction ts1 as [|x t1 ts1 ?? IH] using (map_sorted_ind attr_le);
+        intros n mvs ts2' IHts Hmap.
+      { apply map_Forall2_empty_inv_l in IHts as ->.
+        rewrite map_mapM_sorted_empty in Hmap; simplify_res.
+        by exists (Some ∅), 1. }
+      apply map_Forall2_insert_inv_l in IHts
+        as (t2 & ts2 & -> & ? & IHt & IHts); simplify_eq/=; last done.
+      assert (∀ j, is_Some (ts2 !! j) → attr_le x j).
+      { apply map_Forall2_dom_L in IHts. intros j.
+        rewrite -elem_of_dom -IHts elem_of_dom. auto. }
+      rewrite map_mapM_sorted_insert //= in Hmap.
+      destruct (interp_thunk _ _) as [mv|] eqn:Hinterp; simplify_res.
+      assert (∃ mw m, interp_thunk m t1 = Res mw ∧
+        val_to_expr <$> mv = val_to_expr <$> mw) as (mw & m1 & Hinterp1 & ?).
+      { apply interp_thunk_as_interp in Hinterp as (mw & m & Hinterp & ?).
+        apply IHt in Hinterp as (mw' & m' & Hinterp & ?).
+        eapply interp_as_interp_thunk in Hinterp as (mw'' & m'' & Hinterp & ?).
+        exists mw'', m''. eauto with congruence. }
+      destruct mv as [v|], mw as [w|]; simplify_res; last first.
+      { exists None, m1. split; [|done]. rewrite map_mapM_sorted_insert //=.
+        by rewrite Hinterp1. }
+      destruct (force_deep _ _) as [mv|] eqn:Hforce; simplify_res.
+      eapply force_deep_proper in Hforce as (mw & m2 & Hforce' & ?); last done.
+      destruct mv as [v'|], mw as [w'|]; simplify_res; last first.
+      { exists None, (m1 `max` m2). split; [|done].
+        rewrite map_mapM_sorted_insert //=.
+        rewrite (interp_thunk_le Hinterp1) /=; last lia.
+        rewrite (force_deep_le Hforce') /=; last lia. done. }
+      destruct (map_mapM_sorted _ _ _) as [mvs'|] eqn:Hmap'; simplify_res.
+      apply IH in Hmap' as (mws & m3 & Hmap3 & ?); last done.
+      exists (fmap <[x:=w']> mws), (m1 `max` m2 `max` m3).
+      rewrite map_mapM_sorted_insert //=.
+      rewrite (interp_thunk_le Hinterp1) /=; last lia.
+      rewrite (force_deep_le Hforce') /=; last lia.
+      rewrite (map_mapM_interp_le Hmap3) /=; last lia.
+      destruct mvs', mws; simplify_res; last done.
+      rewrite !fmap_insert. auto with f_equal.
+    + (* DEEP *)
+      assert (map_Forall2 (λ _ t1 t2,
+        thunk_to_expr t1 = thunk_to_expr t2 ∨
+        ∃ v1 v2,
+          thunk_to_expr t1 = val_to_expr v1 ∧
+          thunk_to_expr t2 = val_to_expr v2 ∧
+          ∀ n mv,
+            force_deep n v2 = Res mv →
+            ∃ mw m, force_deep m v1 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw)
+        (<[x:=t1]> ts1) (<[x:=t2]> ts2)) as IHts.
+      { apply map_Forall2_insert_2; last first.
+        { intros y. apply (f_equal (.!! y)) in Hts. rewrite !lookup_fmap in Hts.
+          destruct (ts1 !! y), (ts2 !! y); simplify_eq/=; constructor; eauto. }
+        assert (final SHALLOW (thunk_to_expr t2))
+          as (v2 & m2 & Hinterp2 & Ht2)%final_interp
+          by eauto using step_final_shallow.
+        apply final_interp in Hfinal as (v1 & m1 & Hinterp1 & Ht1); eauto 10. }
+      revert IHts Hmap. generalize (<[x:=t1]> ts1) (<[x:=t2]> ts2). clear.
+      intros ts1. revert n mvs.
+      induction ts1 as [|x t1 ts1 ?? IH] using (map_sorted_ind attr_le);
+        intros n mvs ts2' IHts Hmap.
+      { apply map_Forall2_empty_inv_l in IHts as ->.
+        rewrite map_mapM_sorted_empty in Hmap; simplify_res.
+        by exists (Some ∅), 1. }
+      apply map_Forall2_insert_inv_l in IHts
+        as (t2 & ts2 & -> & ? & IHt & IHts); simplify_eq/=; last done.
+      assert (∀ j, is_Some (ts2 !! j) → attr_le x j).
+      { apply map_Forall2_dom_L in IHts. intros j.
+        rewrite -elem_of_dom -IHts elem_of_dom. auto. }
+      rewrite map_mapM_sorted_insert //= in Hmap.
+      destruct (interp_thunk n t2 ≫= force_deep n)
+        as [mv|] eqn:Hinterp; simplify_res.
+      assert (∃ mw m, interp_thunk m t1 ≫= force_deep m = Res mw ∧
+        val_to_expr <$> mv = val_to_expr <$> mw) as (mw & m1 & Hinterp1 & ?).
+      { destruct (interp_thunk _ _) as [mv'|] eqn:Hthunk; simplify_res.
+        destruct IHt as [|(v1 & v2 & Ht1 & Ht2 & IHt)].
+        * eapply interp_thunk_proper in Hthunk
+            as (mw' & m1 & Hthunk1 & ?); last done.
+          destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+          { exists None, m1. by rewrite Hthunk1. }
+          eapply force_deep_proper in Hinterp
+            as (mw & m2 & Hforce2 & ?); last done.
+          exists mw, (m1 `max` m2). split; [|done].
+          rewrite (interp_thunk_le Hthunk1) /=; last lia.
+          eauto using force_deep_le with lia.
+        * destruct (interp_empty_val_to_expr v1) as (v1' & m1 & Hinterp1 & ?).
+          rewrite -Ht1 in Hinterp1.
+          eapply interp_as_interp_thunk in Hinterp1
+            as ([v1''|] & m1' & Hthunk1 & ?); simplify_res.
+          eapply (interp_thunk_proper _ _ (Forced v2)) in Hthunk
+            as (mw2 & m2 & Hthunk2 & ?); simplify_res; [|done].
+          destruct m2 as [|m2]; [done|].
+          rewrite interp_thunk_S in Hthunk2; simplify_res.
+          destruct mv' as [v2'|]; simplify_res.
+          eapply force_deep_proper in Hinterp
+            as (mv' & m2' & Hforce2 & ?); last done.
+          eapply IHt in Hforce2 as (mw' & m2'' & Hforce2 & ?).
+          eapply (force_deep_proper _ _ v1'') in Hforce2
+            as (mw'' & m2''' & Hforce2 & ?); last congruence.
+          exists mw'', (m1' `max` m2''').
+          rewrite (interp_thunk_le Hthunk1) /=; last lia.
+          rewrite (force_deep_le Hforce2) /=; last lia. auto with congruence. }
+      destruct mv as [v|], mw as [w|]; simplify_res; last first.
+      { exists None, m1. split; [|done]. rewrite map_mapM_sorted_insert //=.
+        by rewrite Hinterp1. }
+      destruct (map_mapM_sorted _ _ _) as [mvs'|] eqn:Hmap'; simplify_res.
+      apply IH in Hmap' as (mws & m2 & Hmap2 & ?); last done.
+      exists (fmap <[x:=w]> mws), (m1 `max` m2).
+      rewrite map_mapM_sorted_insert //=.
+      destruct (interp_thunk m1 t1) as [[]|] eqn:Hinterp'; simplify_res.
+      rewrite (interp_thunk_le Hinterp') /=; last lia.
+      rewrite (force_deep_le Hinterp1) /=; last lia.
+      rewrite (map_mapM_interp_le Hmap2) /=; last lia.
+      destruct mvs', mws; simplify_res; last done.
+      rewrite !fmap_insert. auto with f_equal.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct n as [|n]; simplify_eq/=.
+    rewrite interp_S /= in Hinterp.
+    destruct (interp n ∅ e') as [mv'|] eqn:Hinterp'; simplify_res.
+    apply IHHstep in Hinterp'
+      as (mw' & m1 & Hinterp1 & ?); last by eauto using step_not_final.
+    destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+    { exists None, (S m1). split; [|done]. by rewrite interp_S /= Hinterp1. }
+    eapply interp_app_proper in Hinterp as (mw & m2 & Happ2 & ?); [|done..].
+    exists mw, (S (m1 `max` m2)). rewrite interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia.
+    rewrite (interp_app_le Happ2) /=; last lia. done.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct n as [|[|[|n]]]; simplify_eq/=.
+    rewrite !interp_S /= interp_app_S /= interp_thunk_S /= in Hinterp.
+    destruct (interp n ∅ e') as [mv'|] eqn:Hinterp'; simplify_res.
+    apply IHHstep in Hinterp'
+      as (mw' & m1 & Hinterp1 & Hw'); last by eauto using step_not_final.
+    destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+    { exists None, (S (S (S m1))). split; [|done].
+      rewrite !interp_S /= interp_app_S /= interp_thunk_S /=.
+      by rewrite Hinterp1. }
+    destruct (maybe VAttr v') as [ts|] eqn:?; simplify_res; last first.
+    { exists None, (S (S (S m1))). split; [|done].
+      rewrite !interp_S /= interp_app_S /= interp_thunk_S /= Hinterp1 /=.
+      assert (maybe VAttr w' = None) as ->; [|done].
+      destruct v', w'; naive_solver. }
+    destruct v', w'; simplify_eq/=.
+    rewrite 2!map_fmap_compose in Hw'. apply (inj _) in Hw'.
+    eapply (interp_match_proper ∅ ∅ _ _ ms ms strict) in Hw'; [|done].
+    destruct (interp_match ts _ strict) as [tαs1|] eqn:Hmatch1,
+      (interp_match ts1 _ strict) as [tαs2|] eqn:Hmatch2;
+      simplify_res; try done; last first.
+    { exists None, (S (S (S m1))). split; [|done].
+      rewrite !interp_S /= interp_app_S /= interp_thunk_S /=.
+      rewrite Hinterp1 /= Hmatch2. done. }
+    eapply interp_proper in Hinterp
+      as (mw & m2 & Hinterp & ?); last first.
+    { by apply indirects_env_proper. }
+    exists mw, (S (S (S (m1 `max` m2)))). split; [|done].
+    rewrite !interp_S /= interp_app_S /= interp_thunk_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia.
+    rewrite Hmatch2 /=. eauto using interp_le with lia.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
+    destruct (interp n _ e') as [mv'|] eqn:Hinterp'; simplify_eq/=.
+    destruct (step_any_shallow μ e e') as [|Hfinal]; first done.
+    + apply IHHstep in Hinterp'
+        as (mw' & m & Hinterp' & Hw); last by eauto using step_not_final.
+      destruct mv' as [v|], mw' as [w'|]; simplify_res; last first.
+      { exists None, (S m). by rewrite interp_S /= Hinterp'. }
+      destruct μ; simplify_res.
+      { exists mv, (S (n `max` m)). rewrite interp_S /=.
+        rewrite (interp_le Hinterp') /=; last lia.
+        rewrite (interp_le Hinterp) /=; last lia. done. }
+      destruct (force_deep n v) as [mv'|] eqn:Hforce; simplify_res.
+      eapply force_deep_proper
+        in Hforce as (mw' & m2 & Hforce2 & ?); last done.
+      exists mv, (S (n `max` m `max` m2)). split; [|done]. rewrite interp_S /=.
+      rewrite (interp_le Hinterp') /=; last lia.
+      rewrite (force_deep_le Hforce2) /=; last lia.
+      destruct mv', mw'; simplify_res; eauto using interp_le with lia.
+    + destruct μ; [by odestruct step_not_final|].
+      assert (final SHALLOW e') as (w & m & Hinterp'' & ->)%final_interp
+        by eauto using step_final_shallow.
+      apply interp_empty_val_to_expr_Res in Hinterp'.
+      destruct mv' as [v|]; simplify_res.
+      destruct (force_deep n v) as [mv'|] eqn:Hforce; simplify_res.
+      apply final_interp in Hfinal as (w' & m' & Hinterp''' & ->).
+      eapply IHHstep in Hforce as (mw' & m'' & Hforce' & ?); [|done..].
+      exists mv, (S (n `max` m' `max` m'')). rewrite interp_S /=.
+      rewrite (interp_le Hinterp''') /=; last lia.
+      rewrite (force_deep_le Hforce') /=; last lia.
+      destruct mv', mw'; simplify_res; eauto using interp_le with lia.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
+    destruct (interp n _ _) as [mv'|] eqn:Hinterp'; simplify_eq/=.
+    apply IHHstep in Hinterp'
+      as (mw' & m1 & Hinterp1 & Hw); last by eauto using step_not_final.
+    destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+    { exists None, (S m1). by rewrite interp_S /= Hinterp1. }
+    destruct (maybe VAttr _) eqn:Hattr; simplify_res; last first.
+    { exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
+      by assert (maybe VAttr w' = None) as -> by (by destruct v', w'). }
+    destruct v', w'; simplify_res.
+    rewrite right_id_L in Hinterp.
+    eapply interp_proper in Hinterp as (mw & m2 & Hinterp2 & ?);
+      last by apply subst_env_fmap_proper.
+    exists mw, (S (m1 `max` m2)). rewrite !interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia. rewrite right_id_L.
+    by rewrite (interp_le Hinterp2) /=; last lia.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
+    destruct (interp n _ e') as [mv1|] eqn:Hinterp1; simplify_eq/=.
+    apply IHHstep in Hinterp1 as (mw1 & m & Hinterp1 & Hw1);
+      last by eauto using step_not_final.
+    destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+    { exists None, (S m). by rewrite interp_S /= Hinterp1. }
+    apply (interp_bin_op_proper op) in Hw1.
+    destruct (interp_bin_op _ v1) as [f|] eqn:Hopf; simplify_res; last first.
+    { exists None, (S m). rewrite interp_S /= Hinterp1 /=.
+      by destruct (interp_bin_op _ w1). }
+    destruct (interp_bin_op _ w1) as [g|] eqn:Hopg; simplify_res; [|done].
+    destruct (interp n _ e2) as [mv2|] eqn:Hinterp2; simplify_res.
+    destruct mv2 as [v2|]; simplify_res; last first.
+    { exists None, (S (n `max` m)). split; [|done]. rewrite interp_S /=.
+      rewrite (interp_le Hinterp1) /=; last lia.
+      rewrite (interp_le Hinterp2) /=; last lia. by rewrite Hopg. }
+    specialize (Hw1 v2 _ eq_refl).
+    destruct (f v2) as [t2|], (g v2) as [t2'|] eqn:Hg; simplify_res; last first.
+    { exists None, (S (n `max` m)). split; [|done]. rewrite interp_S /=.
+      rewrite (interp_le Hinterp1) /=; last lia.
+      rewrite (interp_le Hinterp2) /=; last lia. by rewrite Hopg /= Hg. }
+    eapply interp_thunk_proper in Hinterp as (mw & m' & Hthunk & ?); last done.
+    exists mw, (S (n `max` m `max` m')). split; [|done]. rewrite interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia.
+    rewrite (interp_le Hinterp2) /=; last lia. rewrite Hopg /= Hg /=.
+    rewrite (interp_thunk_le Hthunk) /=; last lia. done.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
+    destruct (interp n ∅ e1) as [mw1|] eqn:Hinterp1; simplify_res.
+    apply final_interp in H0 as (v1 & m1 & Hinterp1' & ->).
+    apply interp_bin_op_Some_2 in H1 as [f Hop].
+    assert (mw1 = Some v1) as -> by eauto using interp_agree.
+    rewrite /= Hop /= in Hinterp.
+    destruct (interp _ _ e') as [mv2|] eqn:Hinterp2; simplify_res; last first.
+    apply IHHstep in Hinterp2 as (mw2 & m & Hinterp2 & Hw);
+      last by eauto using step_not_final.
+    destruct mv2 as [v2|], mw2 as [w2|]; simplify_res; last first.
+    { exists None, (S (n `max` m)). split; [|done]. rewrite interp_S /=.
+      rewrite (interp_le Hinterp1) /=; last lia.
+      rewrite (interp_le Hinterp2) /=; last lia. by rewrite Hop. }
+    pose proof @eq_refl as Hf%(interp_bin_op_proper op v1). rewrite !Hop in Hf.
+    apply Hf in Hw; clear Hf.
+    destruct (f v2) as [t|] eqn:Hf,
+      (f w2) as [t'|] eqn:Hf'; simplify_res; last first.
+    { exists None, (S (n `max` m)). split; [|done]. rewrite interp_S /=.
+      rewrite (interp_le Hinterp1) /=; last lia.
+      rewrite (interp_le Hinterp2) /=; last lia. by rewrite Hop /= Hf'. }
+    eapply interp_thunk_proper in Hinterp as (mw & m' & Hthunk & ?); last done.
+    exists mw, (S (n `max` m `max` m')). split; [|done]. rewrite interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia.
+    rewrite (interp_le Hinterp2) /=; last lia. rewrite Hop /= Hf' /=.
+    eauto using interp_thunk_le with lia.
+  - split; [|by intros ? []]. intros n mv _ Hinterp.
+    destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
+    destruct (interp n _ e') as [mv1|] eqn:Hinterp1; simplify_eq/=.
+    apply IHHstep in Hinterp1 as (mw1 & m & Hinterp1 & Hw1);
+      last by eauto using step_not_final.
+    destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+    { exists None, (S m). by rewrite interp_S /= Hinterp1. }
+    exists mv, (S (n `max` m)). split; [|done].
+    rewrite interp_S /= (interp_le Hinterp1) /=; last lia.
+    assert (maybe_VLit w1 ≫= maybe LitBool = maybe_VLit v1 ≫= maybe LitBool) as ->.
+    { destruct v1, w1; repeat destruct select base_lit; naive_solver. }
+    destruct (maybe_VLit v1 ≫= maybe LitBool); simplify_res; [|done].
+    eauto using interp_le with lia.
+Qed.
+
+Lemma final_interp' μ e :
+  final μ e →
+  ∃ w m, interp' m μ ∅ e = mret w ∧ e = val_to_expr w.
+Proof.
+  intros Hfinal. destruct (final_interp _ _ Hfinal) as (w & m & Hinterp & ->).
+  destruct μ.
+  { exists w, m. by rewrite interp_shallow'. }
+  apply final_force_deep' in Hfinal as (w' & m' & Hforce & ?).
+  exists w', (m `max` m'); split; [|done]. rewrite /interp'.
+  rewrite (interp_le Hinterp) /=; last lia. eauto using force_deep_le with lia.
+Qed.
+
+Lemma force_deep_le' {n1 n2 μ v mv} :
+  force_deep' n1 μ v = Res mv → n1 ≤ n2 → force_deep' n2 μ v = Res mv.
+Proof. destruct μ; eauto using force_deep_le. Qed.
+
+Lemma interp_le' {n1 n2 μ E e mv} :
+  interp' n1 μ E e = Res mv → n1 ≤ n2 → interp' n2 μ E e = Res mv.
+Proof.
+  rewrite /interp'. intros.
+  destruct (interp n1 _ _) as [mw|] eqn:Hinterp; simplify_res.
+  rewrite (interp_le Hinterp); last lia.
+  destruct mw; simplify_res; eauto using force_deep_le'.
+Qed.
+
+Lemma interp_agree' {n1 n2 μ E e mv1 mv2} :
+  interp' n1 μ E e = Res mv1 → interp' n2 μ E e = Res mv2 → mv1 = mv2.
+Proof.
+  intros He1 He2. apply (inj Res). destruct (total (≤) n1 n2).
+  - rewrite -He2. symmetry. eauto using interp_le'.
+  - rewrite -He1. eauto using interp_le'.
+Qed.
+
+Lemma interp_step' n μ e1 e2 mv :
+  e1 -{μ}-> e2 →
+  interp' n μ ∅ e2 = Res mv →
+  ∃ mw m, interp' m μ ∅ e1 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  intros Hstep. destruct μ.
+  { setoid_rewrite interp_shallow'.
+    eapply interp_step; eauto using step_not_final. }
+  intros Hinterp. rewrite /interp' in Hinterp.
+  destruct (interp n ∅ e2) as [mv'|] eqn:Hinterp'; simplify_res.
+  destruct (step_any_shallow _ _ _ Hstep) as [|Hfinal].
+  - eapply interp_step in Hinterp' as (mw' & m & Hinterp' & ?);
+      [|by eauto using step_not_final..].
+    destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+    { exists None, m. by rewrite /interp' Hinterp'. }
+    eapply force_deep_proper in Hinterp as (mw' & m' & Hforce & ?); last done.
+    exists mw', (m `max` m'). rewrite /interp'.
+    rewrite (interp_le Hinterp') /=; last lia.
+    eauto using force_deep_le with lia.
+  - assert (final SHALLOW e2)
+      as (w2 & m2 & Hinterpw2 & ->)%final_interp by eauto using step_final_shallow.
+    apply final_interp in Hfinal as (w1 & m1 & Hinterpw1 & ->).
+    apply interp_empty_val_to_expr_Res in Hinterp'; destruct mv'; simplify_res.
+    eapply interp_step in Hstep as [_ Hstep].
+    eapply Hstep in Hinterp as (mw & m & Hforce & ?); [|done..].
+    exists mw, (m `max` m1). split; [|done]. rewrite /interp'.
+    rewrite (interp_le Hinterpw1) /=; last lia.
+    eauto using force_deep_le with lia.
+Qed.
+
+Lemma final_val_to_expr' n μ E e v :
+  interp' n μ E e = mret v → final μ (val_to_expr v).
+Proof.
+  rewrite /interp'. intros Hinterp.
+  destruct (interp _ _ e) as [[w|]|] eqn:Hinterp'; simplify_res.
+  destruct μ; simplify_res; eauto using final_force_deep.
+Qed.
+
+Lemma red_final_interp μ e :
+  red (step μ) e ∨ final μ e ∨ ∃ m, interp' m μ ∅ e = mfail.
+Proof.
+  revert μ. induction e; intros μ'.
+  - (* ELit *)
+    destruct (decide (base_lit_ok b)).
+    + right; left. by constructor.
+    + do 2 right. exists 1. rewrite /interp' interp_S /=. by case_guard.
+  - (* EId *) destruct mkd as [[k d]|].
+    + left. eexists; constructor.
+    + do 2 right. by exists 1.
+  - (* EAbs *) right; left. constructor.
+  - (* EAbsMatch *) right; left. constructor.
+  - (* EApp *) destruct (IHe1 SHALLOW) as [[??]|[Hfinal|[m Hinterp]]].
+    + left. eexists. by eapply SAppL.
+    + apply final_interp in Hfinal as ([] & m & _ & ->); simplify_res.
+      { do 2 right. exists 3. rewrite /interp' interp_S /= interp_lit //. }
+      { left. by repeat econstructor. }
+      { destruct (IHe2 SHALLOW) as [[??]|[Hfinal|[m2 Hinterp2]]].
+        * left. by repeat econstructor.
+        * apply final_interp in Hfinal as (w2 & m2 & Hinterp2 & ->).
+          destruct (maybe VAttr w2) as [ts|] eqn:Hw2; last first.
+          { do 2 right. exists (S (S (S m2))).
+            rewrite /interp' !interp_S /= interp_app_S /= interp_thunk_S /=.
+            rewrite Hinterp2 /= Hw2. done. }
+          destruct w2; simplify_eq/=.
+          destruct (interp_match ts (fmap (M:=option) (subst_env E) <$> ms) strict)
+            as [E'|] eqn:Hmatch; last first.
+          { do 2 right. exists (S (S (S m2))).
+            rewrite /interp' !interp_S /= interp_app_S /= interp_thunk_S /=.
+            rewrite Hinterp2 /= Hmatch. done. }
+          apply interp_match_Some_1 in Hmatch.
+          left. repeat econstructor; [done|].
+          by rewrite map_fmap_compose fmap_attr_expr_Attr.
+        * rewrite interp_shallow' in Hinterp2.
+          do 2 right. exists (S (S (S m2))).
+          rewrite /interp' !interp_S /= interp_app_S /= interp_thunk_S /=.
+          by rewrite Hinterp2. }
+      { do 2 right. by exists 3. }
+      destruct (ts !! "__functor") as [e|] eqn:Hfunc.
+      { left. repeat econstructor; by simplify_map_eq. }
+      do 2 right. exists (S (S m)). rewrite /interp' !interp_S /=.
+      rewrite interp_app_S /= !lookup_fmap Hfunc. done.
+    + rewrite interp_shallow' in Hinterp.
+      do 2 right. exists (S m). by rewrite /interp' interp_S /= Hinterp.
+  - (* ESeq *) destruct (IHe1 μ) as [[??]|[Hfinal|[m Hinterp]]].
+    + left. eexists. by eapply SSeq.
+    + left. by repeat econstructor.
+    + do 2 right. exists (S m). rewrite /interp' interp_S /=.
+      rewrite /interp' in Hinterp.
+      destruct (interp _ _ e1) as [[]|], μ; simplify_res; [|done..].
+      by rewrite Hinterp.
+  - (* EList *)
+    destruct μ'.
+    { right; left. by constructor. }
+    assert (red (step DEEP) (EList es) ∨ Forall (final DEEP) es ∨
+      ∃ m, mapM (mbind (force_deep m) ∘ interp_thunk m)
+             (Thunk ∅ <$> es) = mfail) as Hhelp; last first.
+    { destruct Hhelp as [?|[?|[m Hinterp]]]; [by auto using final..|].
+      do 2 right. exists (S m). rewrite /interp' interp_S /=.
+      rewrite force_deep_S /=. by rewrite Hinterp. }
+    induction H as [|e es He Hes IH]; [by right; left|].
+    destruct (He DEEP) as [[??]|[Hfinal|[m Hinterp]]]; simplify_eq/=.
+    + left. eexists. by eapply (SList []).
+    + destruct IH as [[??]|[?|[m2 Hinterp2]]]; [|by eauto|].
+      * left. inv_step. eexists. eapply (SList (_ :: _)); by eauto.
+      * apply final_interp' in Hfinal as (w & m1 & Hinterp1 & _).
+        do 2 right. exists (S (m1 `max` m2)).
+        rewrite /interp' /force_deep' in Hinterp1.
+        destruct (interp m1 _ _) as [[]|] eqn:Hinterp1'; simplify_res.
+        rewrite interp_thunk_S /= (interp_le Hinterp1') /=; last lia.
+        rewrite (force_deep_le Hinterp1) /=; last lia.
+        rewrite (mapM_interp_le Hinterp2) /=; last lia. done.
+    + do 2 right. exists (S m).
+      rewrite /interp' /force_deep' in Hinterp.
+      destruct (interp m _ _) as [mw|] eqn:Hinterp1'; simplify_res.
+      rewrite interp_thunk_S /= Hinterp1' /=.
+      destruct mw as [w|]; simplify_res; [|done].
+      rewrite (force_deep_le Hinterp) /=; last lia. done.
+  - (* EAttr *) destruct (decide (no_recs αs)) as [Hrecs|]; last first.
+    { left. by repeat econstructor. }
+    destruct μ'.
+    { right; left. by constructor. }
+    assert (red (step DEEP) (EAttr αs) ∨
+      map_Forall (λ _, final DEEP ∘ attr_expr) αs ∨
+      ∃ m, map_mapM_sorted attr_le (mbind (force_deep m) ∘ interp_thunk m)
+             (Thunk ∅ ∘ attr_expr <$> αs) = mfail) as Hhelp; last first.
+    { destruct Hhelp as [?|[?|[m Hinterp]]]; [by auto using final..|].
+      do 2 right. exists (S m). rewrite /interp' interp_S /=.
+      rewrite from_attr_no_recs //. rewrite force_deep_S /=. by rewrite Hinterp. }
+    induction αs as [|x [τ e] es Hx ? IH]
+      using (map_sorted_ind attr_le); [by right; left|].
+    rewrite !map_Forall_insert //.
+    apply map_Forall_insert in H as [He Hes%IH]; clear IH;
+      [|by eauto using no_recs_insert_inv..].
+    assert (τ = NONREC) as -> by (by eapply no_recs_lookup, lookup_insert).
+    assert (∀ y, is_Some ((Thunk ∅ ∘ attr_expr <$> es) !! y) → attr_le x y).
+    { intros y. rewrite lookup_fmap fmap_is_Some. eauto. }
+    destruct (He DEEP) as [[??]|[Hfinal|[m Hinterp]]]; simplify_eq/=.
+    + left. eexists; eapply SAttr; naive_solver eauto using no_recs_insert_inv.
+    + destruct Hes as [[??]|[?|[m2 Hinterp2]]]; [|by eauto|].
+      * left. inv_step; first by naive_solver eauto using no_recs_insert_inv.
+        apply lookup_insert_None in Hx as [??].
+        rewrite insert_commute // in Hrecs. rewrite insert_commute //.
+        eexists; eapply SAttr; [|by rewrite lookup_insert_ne| |done].
+        { eapply no_recs_insert_inv; [|done]. by rewrite lookup_insert_ne. }
+        intros ?? [[<- <-]|[??]]%lookup_insert_Some; eauto.
+      * apply final_interp' in Hfinal as (w & m1 & Hinterp1 & _).
+        do 2 right. exists (S (m1 `max` m2)). rewrite fmap_insert /=.
+        rewrite map_mapM_sorted_insert //=; last by rewrite lookup_fmap Hx.
+        rewrite /interp' /force_deep' in Hinterp1.
+        destruct (interp m1 _ _) as [[]|] eqn:Hinterp1'; simplify_res.
+        rewrite interp_thunk_S /= (interp_le Hinterp1') /=; last lia.
+        rewrite (force_deep_le Hinterp1) /=; last lia.
+        rewrite (map_mapM_interp_le Hinterp2) /=; last lia. done.
+    + do 2 right. exists (S m). rewrite fmap_insert /=.
+      rewrite map_mapM_sorted_insert //=; last by rewrite lookup_fmap Hx.
+      rewrite /interp' /force_deep' in Hinterp.
+      destruct (interp m _ _) as [mw|] eqn:Hinterp'; simplify_res.
+      rewrite interp_thunk_S /= (interp_le Hinterp') /=; last lia.
+      destruct mw as [w|]; simplify_res; [|done].
+      rewrite (force_deep_le Hinterp) /=; last lia. done.
+  - (* ELetAttr *) destruct (IHe1 SHALLOW) as [[??]|[Hfinal|[m Hinterp]]].
+    + left. eexists. by eapply SLetAttr.
+    + apply final_interp in Hfinal as (w & m & Hinterp & ->).
+      destruct (maybe VAttr w) eqn:Hw.
+      { destruct w; simplify_eq/=. left. by repeat econstructor. }
+      do 2 right. exists (S m). by rewrite /interp' interp_S /= Hinterp /= Hw.
+    + do 2 right. exists (S m). rewrite interp_shallow' in Hinterp.
+      by rewrite /interp' interp_S /= Hinterp /=.
+  - (* EBinOp *)
+    destruct (IHe1 SHALLOW) as [[??]|[Hfinal1|[m Hinterp]]].
+    + left. eexists. by eapply SBinOpL.
+    + apply final_interp in Hfinal1 as (w1 & m1 & Hinterp1 & ->).
+      destruct (interp_bin_op op w1) as [f|] eqn:Hop; last first.
+      { do 2 right. exists (S m1). rewrite /interp' interp_S /=.
+        by rewrite Hinterp1 /= Hop. }
+      pose proof Hop as [Φ ?]%interp_bin_op_Some_1.
+      destruct (IHe2 SHALLOW) as [[??]|[Hfinal2|[m Hinterp2]]].
+      * left. by repeat econstructor.
+      * apply final_interp in Hfinal2 as (w2 & m2 & Hinterp2 & ->).
+        destruct (f w2) as [w|] eqn:Hf; last first.
+        ** do 2 right. exists (S (m1 `max` m2)). rewrite /interp' interp_S /=.
+           rewrite (interp_le Hinterp1) /=; last lia.
+           rewrite Hop /= (interp_le Hinterp2) /=; last lia. by rewrite Hf.
+        ** eapply interp_bin_op_Some_Some_1 in Hf as (?&?&?); [|done..].
+           left. by repeat econstructor.
+      * rewrite interp_shallow' in Hinterp2.
+        do 2 right. exists (S (m `max` m1)). rewrite /interp' interp_S /=.
+        rewrite (interp_le Hinterp1) /=; last lia.
+        rewrite Hop /= (interp_le Hinterp2) /=; last lia. done.
+    + rewrite interp_shallow' in Hinterp.
+      do 2 right. exists (S m). by rewrite /interp' interp_S /= Hinterp.
+  - (* EIf *)
+    destruct (IHe1 SHALLOW) as [[??]|[Hfinal1|[m Hinterp]]].
+    + left. eexists. by eapply SIf.
+    + apply final_interp in Hfinal1 as (w1 & m1 & Hinterp1 & ->).
+      destruct (maybe_VLit w1 ≫= maybe LitBool) as [b|] eqn:Hbool; last first.
+      { do 2 right. exists (S m1).
+        rewrite /interp' interp_S /= Hinterp1 /= Hbool. done. }
+      left. destruct w1; repeat destruct select base_lit; simplify_eq/=.
+      eexists; constructor.
+    + rewrite interp_shallow' in Hinterp.
+      do 2 right. exists (S m). by rewrite /interp' interp_S /= Hinterp.
+Qed.
+
+Lemma interp_complete μ e1 e2 :
+  e1 -{μ}->* e2 → nf (step μ) e2 →
+  ∃ mw m, interp' m μ ∅ e1 = Res mw ∧
+    if mw is Some w then e2 = val_to_expr w else ¬final μ e2.
+Proof.
+  intros Hsteps Hnf. induction Hsteps as [e|e1 e2 e3 Hstep _ IH].
+  { destruct (red_final_interp μ  e) as [?|[Hfinal|[m Hinterp]]]; [done|..].
+    - apply final_interp' in Hfinal as (w & m & ? & ?).
+      by exists (Some w), m.
+    - exists None, m. split; [done|]. intros Hfinal.
+      apply final_interp' in Hfinal as (w & m' & Hinterp' & _).
+      rewrite /interp' in Hinterp, Hinterp'.
+      by assert (mfail = mret w) by eauto using interp_agree'. }
+  destruct IH as (mw & m & Hinterp & ?); first done.
+  eapply interp_step' in Hstep as (mw' & m' & ? & ?); last done.
+  destruct mw, mw'; naive_solver.
+Qed.
+
+Lemma interp_complete_ret μ e1 e2 :
+  e1 -{μ}->* e2 → final μ e2 →
+  ∃ w m, interp' m μ ∅ e1 = mret w ∧ e2 = val_to_expr w.
+Proof.
+  intros Hsteps Hfinal. apply interp_complete in Hsteps
+    as ([w|] & m & ? & ?); naive_solver eauto using final_nf.
+Qed.
+Lemma interp_complete_fail μ e1 e2 :
+  e1 -{μ}->* e2 → nf (step μ) e2 → ¬final μ e2 →
+  ∃ m, interp' m μ ∅ e1 = mfail.
+Proof.
+  intros Hsteps Hnf Hfinal.
+  apply interp_complete in Hsteps as ([w|] & m & ? & ?);
+    naive_solver eauto using final_val_to_expr'.
+Qed.
+
+Lemma interp_sound_open n E e mv :
+  interp n E e = Res mv →
+  ∃ e', subst_env E e -{SHALLOW}->* e' ∧
+        if mv is Some v' then e' = val_to_expr v' else stuck SHALLOW e'
+with interp_thunk_sound n t mv :
+  interp_thunk n t = Res mv →
+  ∃ e', thunk_to_expr t -{SHALLOW}->* e' ∧
+        if mv is Some v' then e' = val_to_expr v' else stuck SHALLOW e'
+with interp_app_sound n v1 t2 mv :
+  interp_app n v1 t2 = Res mv →
+  ∃ e', EApp (val_to_expr v1) (thunk_to_expr t2) -{SHALLOW}->* e' ∧
+        if mv is Some v' then e' = val_to_expr v' else stuck SHALLOW e'
+with force_deep_sound n v mv :
+  force_deep n v = Res mv →
+  ∃ e', val_to_expr v -{DEEP}->* e' ∧
+        if mv is Some v' then e' = val_to_expr v' else stuck DEEP e'.
+Proof.
+  - destruct n as [|n]; [done|].
+    rewrite subst_env_eq interp_S. intros Hinterp.
+    destruct e; simplify_res.
+    + (* ELit *) case_guard; simplify_res.
+      * by eexists.
+      * eexists; split; [done|]. split; [|by inv 1]. intros [??]; inv_step.
+    + (* EId *)
+      assert (union_kinded (prod_map id thunk_to_expr <$> E !! x) mke
+      = prod_map id thunk_to_expr <$> (union_kinded (E !! x)
+          (prod_map id (Thunk ∅) <$> mke))) as ->.
+      { destruct (_ !! _) as [[[]]|], mke as [[[]]|];
+          by rewrite /= ?thunk_to_expr_eq /= ?subst_env_empty. }
+      destruct (union_kinded _ _) as [[k t]|]; simplify_res.
+      * apply interp_thunk_sound in Hinterp as (e' & Hsteps & He').
+        exists e'; split; [|done]. eapply rtc_l; [constructor|done].
+      * eexists; split; [done|]. split; [|inv 1]. intros [? Hstep]. inv_step.
+    + (* EAbs *) by eexists.
+    + (* EAbsMatch *) by eexists.
+    + (* EApp *)
+      destruct (interp _ _ _) as [mv1|] eqn:Hinterp1; simplify_res.
+      apply interp_sound_open in Hinterp1 as (e1' & Hsteps1 & He1').
+      destruct mv1 as [v1|]; simplify_res; last first.
+      { eexists; split; [by eapply SAppL_rtc|]. split; [|inv 1].
+        intros [??]. destruct He1' as [Hnf []].
+        inv_step; eauto using final. destruct Hnf; eauto. }
+      apply interp_app_sound in Hinterp as (e' & Hsteps2 & He').
+      eexists e'; split; [|done]. etrans; [|done]. by eapply SAppL_rtc.
+    + (* ESeq *) destruct (interp _ _ e1) as [mv'|] eqn:Hinterp'; simplify_res.
+      apply interp_sound_open in Hinterp' as (e' & Hsteps & He').
+      destruct mv' as [v'|]; simplify_res; last first.
+      { eexists; repeat split; [by apply SSeq_rtc, steps_shallow_any| |inv 1].
+        intros [e'' Hstep]. destruct He' as [Hnf Hfinal].
+        destruct Hfinal. inv_step; eauto using final_any_shallow.
+        apply step_any_shallow in H2 as []; [|done]. destruct Hnf; eauto. }
+      destruct μ; simplify_res.
+      { apply interp_sound_open in Hinterp as (e'' & Hsteps' & He'').
+        eexists; split; [|done]. etrans; first by apply SSeq_rtc.
+        eapply rtc_l; first by apply SSeqFinal. done. }
+      destruct (force_deep _ _) as [mw|] eqn:Hforce; simplify_res.
+      pose proof Hforce as Hforce'.
+      apply force_deep_sound in Hforce' as (e'' & Hsteps' & He'').
+      destruct mw as [w|]; simplify_res; last first.
+      { eexists. split.
+        { etrans; [by eapply SSeq_rtc, steps_shallow_any|].
+          etrans; [by eapply SSeq_rtc|]. done. }
+        split; [|inv 1]. destruct He''. intros [e''' Hstep].
+        inv_step; eauto using step_not_final. }
+      apply interp_sound_open in Hinterp as (e''' & Hsteps'' & He''').
+      exists e'''. split; [|done].
+      etrans; [by eapply SSeq_rtc, steps_shallow_any|].
+      etrans; [by eapply SSeq_rtc|].
+      eapply rtc_l; first by eapply SSeqFinal, final_force_deep. done.
+    + (* EList *)
+      eexists; split; [done|]. f_equal.
+      induction es; f_equal/=; auto.
+    + (* EAttr *)
+      eexists; split; [apply SAttr_rec_rtc|].
+      f_equal. apply map_eq=> x. rewrite !lookup_fmap.
+      destruct (αs !! x) as [[[] e]|] eqn:?; do 2 f_equal/=.
+      by rewrite subst_env_indirects_env_attr_to_tattr.
+    + (* ELetAttr *) destruct (interp _ _ _) as [mv'|] eqn:Hinterp'; simplify_res.
+      apply interp_sound_open in Hinterp' as (e' & Hsteps & He').
+      destruct mv' as [v'|]; simplify_res; last first.
+      { eexists; repeat split; [by apply SLetAttr_rtc| |inv 1].
+        intros [e'' Hstep]. destruct He' as [Hnf Hfinal].
+        inv_step; [by destruct Hfinal; constructor|]. destruct Hnf; eauto. }
+      destruct (maybe VAttr v') eqn:?; simplify_res; last first.
+      { eexists; repeat split; [by apply SLetAttr_rtc| |inv 1].
+        intros [e'' Hstep]. destruct v'; inv_step; simplify_eq/=. }
+      destruct v'; simplify_res.
+      apply interp_sound_open in Hinterp as (e'' & Hsteps' & He'').
+      eexists; split; [|done]. etrans; [by apply SLetAttr_rtc|].
+      eapply rtc_l; [by econstructor|].
+      rewrite subst_env_union in Hsteps'.
+      rewrite subst_env_alt -!map_fmap_compose in Hsteps'.
+      by rewrite -map_fmap_compose.
+    + (* EBinOp *)
+      destruct (interp _ _ e1) as [mv1|] eqn:Hinterp1; simplify_res.
+      apply interp_sound_open in Hinterp1 as (e1' & Hsteps1 & He1').
+      destruct mv1 as [v1|]; simplify_res; last first.
+      { eexists; split; [by eapply SBinOpL_rtc|]. split; [|inv 1].
+        intros [? Hstep]. destruct He1'. inv_step; naive_solver. }
+      destruct (interp_bin_op _ v1) as [f|] eqn:Hop; simplify_res; last first.
+      { assert (¬∃ Φ, sem_bin_op op (val_to_expr v1) Φ).
+        { by intros [? ?%interp_bin_op_Some_2%not_eq_None_Some]. }
+        eexists; split; [by eapply SBinOpL_rtc|]. split; [|inv 1].
+        intros [? Hstep]. inv_step; eauto using step_not_val_to_expr. }
+      pose proof Hop as [Φ ?]%interp_bin_op_Some_1.
+      destruct (interp _ _ e2) as [mv2|] eqn:Hinterp2; simplify_res.
+      apply interp_sound_open in Hinterp2 as (e2' & Hsteps2 & He2').
+      destruct mv2 as [v2|]; simplify_res; last first.
+      { eexists; split.
+        { etrans; [by eapply SBinOpL_rtc|].
+          eapply SBinOpR_rtc; eauto using interp_bin_op_Some_1. }
+        split; [|inv 1]. destruct He2'.
+        intros [? Hstep]. inv_step; eauto using step_not_val_to_expr. }
+      destruct (f v2) eqn:Hf; simplify_res; last first.
+      { eexists; split.
+        { etrans; [by eapply SBinOpL_rtc|].
+          eapply SBinOpR_rtc; eauto using interp_bin_op_Some_1. }
+        split; [|inv 1]. pose proof @interp_bin_op_Some_Some_2.
+        intros [? Hstep]. inv_step; naive_solver eauto using step_not_val_to_expr. }
+      apply interp_thunk_sound in Hinterp as (e' & Hsteps3 & He').
+      eapply interp_bin_op_Some_Some_1 in Hf as (e3 & ? & ?); [|done..].
+      eapply delayed_steps_l in Hsteps3
+        as (e'' & Hsteps3 & Hdel); last done.
+      eexists e''; split.
+      { etrans; [by eapply SBinOpL_rtc|].
+        etrans; [eapply SBinOpR_rtc; eauto using interp_bin_op_Some_1|].
+        eapply rtc_l; [by econstructor|]. done. }
+      destruct mv.
+      { subst e'. eapply delayed_final_l in Hdel as <-; done. }
+      destruct He' as [Hnf Hfinal]. split.
+      { intros [e4 Hsteps4]. destruct Hnf.
+        eapply delayed_step_r in Hsteps4 as (e4' & Hstep4' & ?); [|done].
+        destruct Hstep4'; eauto. }
+      intros Hfinal'. eapply Hnf.
+      eapply delayed_final_r in Hfinal' as Hsteps; [|done].
+      destruct Hsteps; by eauto.
+    + (* EIf *)
+      destruct (interp _ _ e1) as [mv1|] eqn:Hinterp1; simplify_res.
+      apply interp_sound_open in Hinterp1 as (e1' & Hsteps1 & He1').
+      destruct mv1 as [v1|]; simplify_res; last first.
+      { eexists; repeat split; [by apply SIf_rtc| |inv 1].
+        intros [e'' Hstep]. destruct He1' as [Hnf Hfinal].
+        destruct Hfinal. inv_step; eauto using final. destruct Hnf; eauto. }
+      destruct (maybe_VLit v1 ≫= maybe LitBool) as [b|] eqn:Hbool;
+        simplify_res; last first.
+      { eexists; repeat split; [by apply SIf_rtc| |inv 1].
+        intros [e'' ?]. destruct v1; inv_step; eauto using final. }
+      apply interp_sound_open in Hinterp as (e' & Hsteps & He').
+      exists e'; split; [|done]. etrans; [by apply SIf_rtc|].
+      assert (val_to_expr v1 = ELit (LitBool b)) as ->.
+      { destruct v1; repeat destruct select base_lit; naive_solver. }
+      eapply rtc_l; [constructor|]. by destruct b.
+  - destruct n as [|n]; [done|]. rewrite interp_thunk_S /=.
+    intros Hthunk. destruct t; simplify_res; [by eauto using rtc..|].
+    destruct (tαs !! x) as [[e|t]|] eqn:Hx; simplify_res.
+    + apply interp_sound_open in Hthunk as (e' & Hsteps & ?).
+      exists e'; split; [|done]. etrans; [eapply SBinOpL_rtc, SAttr_rec_rtc|].
+      eapply rtc_l; [eapply SBinOp; repeat constructor|]; try done; simpl.
+      eexists; split; [done|]. rewrite !lookup_fmap Hx /=.
+      rewrite -subst_env_indirects_env_attr_to_tattr_empty.
+      by rewrite -subst_env_indirects_env.
+    + apply interp_thunk_sound in Hthunk as (e' & Hsteps & ?).
+      exists e'; split; [|done]. etrans; [eapply SBinOpL_rtc, SAttr_rec_rtc|].
+      eapply rtc_l; [eapply SBinOp; repeat constructor|]; try done; simpl.
+      eexists; split; [done|]. by rewrite !lookup_fmap Hx /=.
+    + eexists. split; [eapply SBinOpL_rtc, SAttr_rec_rtc|]. split; [|inv 1].
+      intros [??]. inv_step. inv H7. destruct H8 as (? & ? & Hx'); simplify_eq/=.
+      by rewrite !lookup_fmap Hx in Hx'.
+  - destruct n as [|n]; [done|]. rewrite interp_app_S /=. intros Happ.
+    destruct v1; simplify_res.
+    + eexists; split; [done|]. split; [|inv 1]. intros [??]; inv_step.
+    + eapply interp_sound_open in Happ as (e' & Hsteps & He').
+      eexists; split; [|done]. eapply rtc_l; [constructor|].
+      rewrite subst_abs_env_insert // in Hsteps.
+    + destruct (interp_thunk _ _) as [mv'|] eqn:Hthunk; simplify_res.
+      apply interp_thunk_sound in Hthunk as (et & Htsteps & Het).
+      destruct mv' as [v'|]; simplify_res; last first.
+      { eexists; split; [by eapply SAppR_rtc|].
+        split; [|inv 1]. destruct Het.
+        intros [??]; inv_step; eauto using final. }
+      destruct (maybe VAttr v') as [ts|] eqn:?; simplify_res; last first.
+      { eexists; repeat split; [by apply SAppR_rtc| |inv 1].
+        intros [e'' Hstep]. destruct v'; inv_step; simplify_eq/=. }
+      destruct v'; simplify_res.
+      destruct (interp_match _ _ _) as [tαs|] eqn:Hmatch;
+        simplify_res; last first.
+      { eexists; repeat split; [by apply SAppR_rtc| |inv 1].
+        intros [e'' Hstep]. inv_step.
+        rewrite map_fmap_compose fmap_attr_expr_Attr in H6.
+        apply interp_match_Some_2 in H6. rewrite interp_match_subst in H6.
+        opose proof (interp_match_proper ∅ ∅
+          (Thunk ∅ <$> (thunk_to_expr <$> ts)) ts ms ms strict _ _).
+        { apply map_eq=> x. rewrite !lookup_fmap.
+          destruct (ts !! x); f_equal/=. by rewrite subst_env_empty. }
+        { done. }
+        repeat destruct (interp_match _ _ _); simplify_eq/=. }
+      pose proof (interp_match_subst E ts ms strict) as Hmatch'.
+      rewrite Hmatch /= in Hmatch'.
+      apply interp_match_Some_1 in Hmatch'.
+      apply interp_sound_open in Happ as (e' & Hsteps & ?).
+      exists e'; split; [|done].
+      etrans; [by apply SAppR_rtc|].
+      eapply rtc_l; [constructor; [done|]|].
+      { rewrite map_fmap_compose fmap_attr_expr_Attr. done. }
+      etrans; [|apply Hsteps]. apply reflexive_eq. f_equal.
+      rewrite subst_env_indirects_env.
+      rewrite subst_env_indirects_env_attr_to_tattr_empty.
+      do 2 f_equal. apply map_eq=> y. rewrite !lookup_fmap.
+      destruct (_ !! y) as [[]|]; f_equal/=. by rewrite subst_env_empty.
+    + eexists; split; [done|]. split; [|inv 1]. intros [??]; inv_step.
+    + destruct (ts !! _) eqn:Hfunc; simplify_res; last first.
+      { eexists; split; [by eapply SAppL_rtc|]. split; [|inv 1].
+        intros [??]; inv_step; simplify_map_eq. }
+      destruct (interp_thunk _ _) as [mv'|] eqn:Hthunk; simplify_res.
+      apply interp_thunk_sound in Hthunk as (et & Htsteps & Het).
+      assert (EApp (EAttr (AttrN ∘ thunk_to_expr <$> ts)) (thunk_to_expr t2)
+        -{SHALLOW}->*
+        EApp (EApp et (EAttr (AttrN ∘ thunk_to_expr <$> ts))) (thunk_to_expr t2))
+        as Hsteps; [|clear Htsteps].
+      { eapply rtc_l; [constructor; by simplify_map_eq|].
+        eapply SAppL_rtc, SAppL_rtc, Htsteps. }
+      destruct mv' as [v'|]; simplify_res; last first.
+      { eexists; split; [exact Hsteps|].
+        split; [|inv 1]. intros [??]. destruct Het as [Hnf []].
+        inv_step; eauto using final. destruct Hnf; eauto. }
+      destruct (interp_app _ _ _) as [mv'|] eqn:Happ'; simplify_res.
+      apply interp_app_sound in Happ' as (e' & Hsteps' & He').
+      destruct mv' as [v''|]; simplify_res; last first.
+      { eexists; split; [etrans; [apply Hsteps|apply SAppL_rtc, Hsteps']|].
+        split; [|inv 1]. intros [??]. destruct He' as [Hnf []].
+        inv_step; eauto using final. destruct Hnf; eauto. }
+      apply interp_app_sound in Happ as (e'' & Hsteps'' & He'').
+      eexists e''; split; [|done].
+      etrans; [apply Hsteps|]. etrans; [apply SAppL_rtc, Hsteps'|]. done.
+  - destruct n as [|n]; [done|]. rewrite force_deep_S.
+    intros Hforce. destruct v; simplify_res.
+    + (* VLit *) by eexists.
+    + (* VAbs *) by eexists.
+    + (* VAbsMatch *) by eexists.
+    + (* VList *)
+      destruct (mapM _ _) as [mvs|] eqn:Hmap; simplify_res.
+      assert (∃ ts',
+        EList (thunk_to_expr <$> ts) -{DEEP}->* EList (thunk_to_expr <$> ts') ∧
+        if mvs is Some vs then thunk_to_expr <$> ts' = val_to_expr <$> vs
+        else nf (step DEEP) (EList (thunk_to_expr <$> ts')) ∧
+          ¬Forall (final DEEP ∘ thunk_to_expr) ts')
+        as (ts' & Hsteps & Hts'); last first.
+      { eexists; split; [done|]. destruct mvs as [vs|]; simplify_eq/=.
+        * f_equal. rewrite -list_fmap_compose Hts'.
+          clear. induction vs; f_equal/=; auto.
+        * destruct Hts' as [Hnf Hfinal]; split; [done|].
+          inv 1. by apply Hfinal, Forall_fmap. }
+      revert mvs Hmap. induction ts as [|t ts IH]; intros mv' Hmap; simplify_res.
+      { by exists []. }
+      destruct (interp_thunk _ _) as [mv''|] eqn:Hthunk; simplify_res.
+      apply interp_thunk_sound in Hthunk as (et & Htsteps & Het).
+      destruct mv'' as [v''|]; simplify_res; last first.
+      { exists (Thunk ∅ et :: ts); csimpl. rewrite subst_env_empty.
+        apply (stuck_shallow_any DEEP) in Het as [??]. split_and!.
+        * eapply (SList_rtc []); [done|].
+          etrans; [by apply steps_shallow_any|done].
+        * by apply List_nf_cons.
+        * rewrite Forall_cons /= subst_env_empty.
+          naive_solver eauto using final_any_shallow. }
+      destruct (force_deep _ _) as [mvf|] eqn:Hforce; simplify_res.
+      pose proof Hforce as Hforce'.
+      apply force_deep_sound in Hforce' as (e' & Hsteps' & He').
+      destruct mvf as [vf|]; simplify_res; last first.
+      { exists (Thunk ∅ e' :: ts). csimpl. rewrite subst_env_empty.
+        destruct He'. split_and!.
+        * eapply (SList_rtc []); [done|].
+          etrans; [by apply steps_shallow_any|done].
+        * by apply List_nf_cons.
+        * rewrite Forall_cons /= subst_env_empty. naive_solver. }
+      destruct (mapM _ _) as [mvs|] eqn:Hmap'; simplify_res.
+      destruct (IH _ eq_refl) as (ts' & Hsteps'' & Hts').
+      exists (Forced vf :: ts'); csimpl. split.
+      { etrans; [eapply (SList_rtc []); [done..|];
+          etrans; [by apply steps_shallow_any|done]|]; simpl.
+        eapply List_steps_cons; by eauto using final_force_deep. }
+      destruct mvs as [vs|]; simplify_res.
+      { by rewrite Hts'. }
+      split; [|rewrite Forall_cons; naive_solver].
+      apply List_nf_cons_final; naive_solver eauto using final_force_deep.
+    + (* VAttr *)
+      destruct (map_mapM_sorted _ _) as [mvs|] eqn:Hmap; simplify_res.
+      assert (∃ ts',
+        EAttr (AttrN ∘ thunk_to_expr <$> ts) -{DEEP}->*
+          EAttr (AttrN ∘ thunk_to_expr <$> ts') ∧
+        if mvs is Some vs then thunk_to_expr <$> ts' = val_to_expr <$> vs
+        else nf (step DEEP) (EAttr (AttrN ∘ thunk_to_expr <$> ts')) ∧
+          ¬map_Forall (λ _, final DEEP ∘ thunk_to_expr) ts')
+        as (ts' & Hsteps & Hts'); last first.
+      { eexists; split; [done|]. destruct mvs as [vs|]; simplify_eq/=.
+        * f_equal. rewrite map_fmap_compose Hts'.
+          apply map_eq=> x. rewrite !lookup_fmap. by destruct (vs !! x).
+        * destruct Hts' as [Hnf Hfinal]; split; [done|].
+          inv 1. apply Hfinal=> x t Hx /=.
+          ospecialize (H2 x _ _); first by rewrite lookup_fmap Hx. done. }
+      revert mvs Hmap. induction ts as [|x t ts Hx ? IH]
+        using (map_sorted_ind attr_le); intros mv' Hmap.
+      { rewrite map_mapM_sorted_empty in Hmap; simplify_res. by exists ∅. }
+      rewrite map_mapM_sorted_insert //= in Hmap.
+      assert ((AttrN ∘ thunk_to_expr <$> ts) !! x = None).
+      { by rewrite lookup_fmap Hx. }
+      assert (∀ y α, (AttrN ∘ thunk_to_expr <$> ts) !! y = Some α →
+        final DEEP (attr_expr α) ∨ attr_le x y).
+      { intros y α. rewrite lookup_fmap. destruct (ts !! y) eqn:?; naive_solver. }
+      destruct (interp_thunk _ _) as [mv''|] eqn:Hthunk; simplify_res.
+      apply interp_thunk_sound in Hthunk as (et & Htsteps & Het).
+      destruct mv'' as [v''|]; simplify_res; last first.
+      { exists (<[x:=Thunk ∅ et]> ts).
+        rewrite !fmap_insert /= subst_env_empty.
+        apply (stuck_shallow_any DEEP) in Het as [??]. split_and!.
+        * eapply SAttr_lookup_rtc; [done..|].
+          etrans; [by apply steps_shallow_any|done].
+        * apply Attr_nf_insert; auto.
+          intros y. rewrite lookup_fmap fmap_is_Some. eauto.
+        * rewrite map_Forall_insert //= subst_env_empty.
+          naive_solver eauto using final_any_shallow. }
+      destruct (force_deep _ _) as [mvf|] eqn:Hforce; simplify_res.
+      pose proof Hforce as Hforce'.
+      apply force_deep_sound in Hforce' as (e' & Hsteps' & He').
+      destruct mvf as [vf|]; simplify_res; last first.
+      { exists (<[x:=Thunk ∅ e']> ts). rewrite !fmap_insert /= subst_env_empty.
+        destruct He'. split_and!.
+        * eapply SAttr_lookup_rtc; [done..|].
+          etrans; [by apply steps_shallow_any|done].
+        * apply Attr_nf_insert; auto.
+          intros y. rewrite lookup_fmap fmap_is_Some. eauto.
+        * rewrite map_Forall_insert //= subst_env_empty. naive_solver. }
+      destruct (map_mapM_sorted _ _ _) as [mvs|] eqn:Hmap'; simplify_res.
+      destruct (IH _ eq_refl) as (ts' & Hsteps'' & Hts').
+      exists (<[x:=Forced vf]> ts'). split.
+      { rewrite !fmap_insert /=.
+        etrans; [eapply SAttr_lookup_rtc; [done..|];
+          etrans; [by apply steps_shallow_any|done]|].
+        eapply Attr_steps_insert; by eauto using final_force_deep. }
+      destruct mvs as [vs|]; simplify_res.
+      { by rewrite !fmap_insert Hts'. }
+      assert (∀ y, ts !! y = None ↔ ts' !! y = None) as Hdom.
+      { intros y. rewrite -!(fmap_None (AttrN ∘ thunk_to_expr)).
+        rewrite -!lookup_fmap. by eapply Attr_steps_dom. }
+      split; [|rewrite map_Forall_insert; naive_solver].
+      rewrite fmap_insert /=. apply Attr_nf_insert_final;
+        eauto using final_force_deep.
+      * rewrite lookup_fmap fmap_None. naive_solver.
+      * intros y. rewrite lookup_fmap fmap_is_Some.
+        rewrite -not_eq_None_Some -Hdom not_eq_None_Some. auto.
+      * naive_solver.
+Qed.
+
+Lemma interp_sound_open' n μ E e mv :
+  interp' n μ E e = Res mv →
+  ∃ e', subst_env E e -{μ}->* e' ∧
+        if mv is Some v' then e' = val_to_expr v' else stuck μ e'.
+Proof.
+  intros Hinterp. destruct μ.
+  { rewrite interp_shallow' in Hinterp. by eapply interp_sound_open. }
+  rewrite /interp' /= in Hinterp.
+  destruct (interp n E e) as [mv'|] eqn:Hinterp'; simplify_res.
+  apply interp_sound_open in Hinterp' as (e' & Hsteps & He').
+  destruct mv' as [v'|]; simplify_res; last first.
+  { eauto using steps_shallow_any, stuck_shallow_any. }
+  eapply force_deep_sound in Hinterp as (e'' & Hsteps' & He'').
+  eexists; split; [|done]. etrans; [by eapply steps_shallow_any|done].
+Qed.
+
+Lemma interp_sound n μ e mv :
+  interp' n μ ∅ e = Res mv →
+  ∃ e', e -{μ}->* e' ∧
+        if mv is Some v then e' = val_to_expr v else stuck μ e'.
+Proof.
+  intros Hsteps%interp_sound_open'. by rewrite subst_env_empty in Hsteps.
+Qed.
+
+(** Final theorems *)
+Theorem interp_sound_complete_ret e v :
+  (∃ w n, interp' n SHALLOW ∅ e = mret w ∧ val_to_expr v = val_to_expr w)
+    ↔ e -{SHALLOW}->* val_to_expr v.
+Proof.
+  split.
+  - by intros (n & w & (e' & ? & ->)%interp_sound & ->).
+  - intros Hsteps. apply interp_complete in Hsteps as ([] & ? & ? & ?);
+      unfold nf, red;
+      naive_solver eauto using final_val_to_expr, step_not_val_to_expr.
+Qed.
+
+Theorem interp_sound_complete_ret_lit μ e bl (Hbl : base_lit_ok bl) :
+  (∃ n, interp' n μ ∅ e = mret (VLit bl Hbl)) ↔ e -{μ}->* ELit bl.
+Proof.
+  split.
+  - intros [n (e' & ? & ->)%interp_sound]. done.
+  - intros Hsteps. apply interp_complete_ret in Hsteps
+      as ([] & n & ? & Hv); simplify_eq/=; last by constructor.
+    exists n. by rewrite (proof_irrel Hbl Hbl0).
+Qed.
+
+Theorem interp_sound_complete_fail μ e :
+  (∃ n, interp' n μ ∅ e = mfail) ↔ ∃ e', e -{μ}->* e' ∧ stuck μ e'.
+Proof.
+  split.
+  - by intros [n ?%interp_sound].
+  - intros (e' & Hsteps & Hnf & Hfinal). by eapply interp_complete_fail.
+Qed.
+
+Theorem interp_sound_complete_no_fuel μ e :
+  (∀ n, interp' n μ ∅ e = NoFuel) ↔ all_loop (step μ) e.
+Proof.
+  rewrite all_loop_alt. split.
+  - intros Hnofuel e' Hsteps.
+    destruct (red_final_interp μ e') as [|[|He']]; [done|..].
+    + apply interp_complete_ret in Hsteps as (w & m & Hinterp & _); last done.
+      by rewrite Hnofuel in Hinterp.
+    + apply interp_sound_complete_fail in He' as (e'' & ? & [Hnf _]).
+      destruct (interp_complete μ e e'')
+        as (mv & n & Hinterp & _); [by etrans|done|].
+      by rewrite Hnofuel in Hinterp.
+  - intros Hred n. destruct (interp' n μ ∅ e) as [mv|] eqn:Hinterp; [|done].
+    destruct (interp_sound _ _ _ _ Hinterp) as (e' & Hsteps & Hstuck).
+    destruct mv as [v|]; simplify_eq/=.
+    + apply Hred in Hsteps as []%final_nf. by eapply final_val_to_expr'.
+    + destruct Hstuck as [[] ?]; eauto.
+Qed.