diff --git a/_CoqProject b/_CoqProject
index 0245b90bd30fbcf5ba8fbda67fc0c0c56c17a86e..2be3857d606d2c10606a2ceb651608f231c2c6c5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,6 +7,5 @@ memcpy.v
 notation.v
 proofmode.v
 races.v
-substitution.v
 tactics.v
 wp_tactics.v
diff --git a/derived.v b/derived.v
index 71a63a67158afb062e9250579e5e53aae6560ff1..b6f092b1ac57adadc5be1b203ecf063158548ff4 100644
--- a/derived.v
+++ b/derived.v
@@ -21,18 +21,18 @@ Implicit Types P Q : iProp lrust_lang Σ.
 Implicit Types Φ : val → iProp lrust_lang Σ.
 
 (** Proof rules for the sugar *)
-Lemma wp_lam E xl e e' el Φ :
+Lemma wp_lam E xl e `{Closed (omap (maybe BNamed) xl) e} e' el Φ :
   Forall (λ ei, is_Some (to_val ei)) el →
   subst_l xl el e = Some e' →
   ▷ WP e' @ E {{ Φ }} ⊢ WP App (Lam xl e) el @ E {{ Φ }}.
 Proof. iIntros (??) "?". by iApply (wp_rec _ BAnon). Qed.
 
-Lemma wp_let E x e1 e2 v Φ :
+Lemma wp_let E x e1 e2 `{Closed (option_list (maybe BNamed x)) e2} v Φ :
   to_val e1 = Some v →
   ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
 Proof. eauto using wp_lam. Qed.
 
-Lemma wp_seq E e1 e2 v Φ :
+Lemma wp_seq E e1 e2 `{Closed [] e2} v Φ :
   to_val e1 = Some v →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
 Proof. iIntros (?) "?". by iApply (wp_let _ BAnon). Qed.
diff --git a/lang.v b/lang.v
index 9f0ed76cf9314f68f8c0bc940f614c3093daa2c2..ef2ce9bf64b1c2113d5d9941cdd3f884f3e6594b 100644
--- a/lang.v
+++ b/lang.v
@@ -20,101 +20,89 @@ Inductive binder := BAnon | BNamed : string → binder.
 Delimit Scope lrust_binder_scope with RustB.
 Bind Scope lrust_binder_scope with binder.
 
-Definition cons_binder (mx : binder) (X : list string) : list string :=
-  match mx with BAnon => X | BNamed x => x :: X end.
-Infix ":b:" := cons_binder (at level 60, right associativity).
-Fixpoint app_binder (mxl : list binder) (X : list string) : list string :=
-  match mxl with [] => X | b :: mxl => b :b: app_binder mxl X end.
-Infix "+b+" := app_binder (at level 60, right associativity).
+Instance bnamed_maybe : Maybe (BNamed) :=
+  λ x, match x with BNamed y => Some y | _ => None end.
+
 Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
 Proof. solve_decision. Defined.
 
-Instance set_unfold_cons_binder x mx X P :
-  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
-Proof.
-  constructor. rewrite -(set_unfold (x ∈ X) P).
-  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
-Qed.
-Instance set_unfold_app_binder x mxl X P :
-  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mxl +b+ X) (BNamed x ∈ mxl ∨ P).
-Proof.
-  constructor. rewrite -(set_unfold (x ∈ X) P).
-  induction mxl as [|?? IH]; set_solver.
-Qed.
-
-(** A typeclass for whether a variable is bound in a given
-   context. Making this a typeclass means we can use typeclass search
-   to program solving these constraints, so this becomes extensible.
-   Also, since typeclass search runs *after* unification, Coq has already
-   inferred the X for us; if we were to go for embedded proof terms ot
-   tactics, Coq would do things in the wrong order. *)
-Class VarBound (x : string) (X : list string) :=
-  var_bound : bool_decide (x ∈ X).
-(* There is no need to restrict this hint to terms without evars, [vm_compute]
-will fail in case evars are arround. *)
-Hint Extern 0 (VarBound _ _) => vm_compute; exact I : typeclass_instances.
-
-Instance var_bound_proof_irrel x X : ProofIrrel (VarBound x X).
-Proof. rewrite /VarBound. apply _. Qed.
-Instance set_unfold_var_bound x X P :
-  SetUnfold (x ∈ X) P → SetUnfold (VarBound x X) P.
-Proof.
-  constructor. by rewrite /VarBound bool_decide_spec (set_unfold (x ∈ X) P).
-Qed.
-
-Inductive expr (X : list string) :=
-(* Var is the only place where the terms contain a proof. The fact that they
-   contain a proof at all is suboptimal, since this means two seeminlgy
-   convertible terms could differ in their proofs. However, this also has
-   some advantages:
-   * We can make the [X] an index, so we can do non-dependent match.
-   * In expr_weaken, we can push the proof all the way into Var, making
-     sure that proofs never block computation. *)
-| Var (x : string) `{VarBound x X}
+Inductive expr :=
+| Var (x : string)
 | Lit (l : base_lit)
-| Rec (f : binder) (xl : list binder) (e : expr (xl +b+ f :b: X))
-| BinOp (op : bin_op) (e1 e2 : expr X)
-| App (e : expr X) (el : list (expr X))
-| Read (o : order) (e : expr X)
-| Write (o : order) (e1 e2: expr X)
-| CAS (e0 e1 e2 : expr X)
-| Alloc (e : expr X)
-| Free (e1 e2 : expr X)
-| Case (e : expr X) (el : list (expr X))
-| Fork (e : expr X).
+| Rec (f : binder) (xl : list binder) (e : expr)
+| BinOp (op : bin_op) (e1 e2 : expr)
+| App (e : expr) (el : list expr)
+| Read (o : order) (e : expr)
+| Write (o : order) (e1 e2: expr)
+| CAS (e0 e1 e2 : expr)
+| Alloc (e : expr)
+| Free (e1 e2 : expr)
+| Case (e : expr) (el : list expr)
+| Fork (e : expr).
 
 Bind Scope lrust_expr_scope with expr.
 Bind Scope lrust_expr_scope with list expr.
 Delimit Scope lrust_expr_scope with RustE.
-Arguments Var {_} _ {_}.
-Arguments Lit {_} _.
-Arguments Rec {_} _ _ _%RustE.
-Arguments BinOp {_} _ _%RustE _%RustE.
-Arguments App {_} _%RustE _%RustE.
-Arguments Read {_} _ _%RustE.
-Arguments Write {_} _ _%RustE _%RustE.
-Arguments CAS {_} _%RustE _%RustE _%RustE.
-Arguments Alloc {_} _%RustE.
-Arguments Free {_} _%RustE _%RustE.
-Arguments Case {_} _%RustE _%RustE.
-Arguments Fork {_} _%RustE.
+Arguments Var _.
+Arguments Lit _.
+Arguments Rec _ _ _%RustE.
+Arguments BinOp _ _%RustE _%RustE.
+Arguments App _%RustE _%RustE.
+Arguments Read _ _%RustE.
+Arguments Write _ _%RustE _%RustE.
+Arguments CAS _%RustE _%RustE _%RustE.
+Arguments Alloc _%RustE.
+Arguments Free _%RustE _%RustE.
+Arguments Case _%RustE _%RustE.
+Arguments Fork _%RustE.
+
+Fixpoint is_closed (env : list string) (e : expr) : bool :=
+  match e with
+  | Var x => bool_decide (x ∈ env)
+  | Lit _ => true
+  | Rec f xl e =>
+    is_closed
+      (foldr (λ x, match x with BAnon => id | BNamed x => (x ::) end)
+             env (f::xl))
+      e
+  | BinOp _ e1 e2 | Write _ e1 e2 | Free e1 e2 =>
+    is_closed env e1 && is_closed env e2
+  | App e el | Case e el => foldr (λ e, andb (is_closed env e)) (is_closed env e) el
+  | Read _ e | Alloc e | Fork e => is_closed env e
+  | CAS e0 e1 e2 => is_closed env e0 && is_closed env e1 && is_closed env e2
+  end.
+
+Class Closed (env : list string) (e : expr) :=
+  closed : is_closed env e.
+(* There is no need to restrict this hint to terms without evars, [vm_compute]
+will fail in case evars are arround. *)
+Hint Extern 0 (Closed _ _) => vm_compute; exact I : typeclass_instances.
+Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
+Proof. rewrite /Closed. apply _. Qed.
+Instance closed_decision env e : Decision (Closed env e).
+Proof. rewrite /Closed. apply _. Qed.
 
 Inductive val :=
 | LitV (l : base_lit)
-| RecV (f : binder) (xl : list binder) (e : expr (xl +b+ f :b: [])).
+| RecV (f : binder) (xl : list binder) (e : expr)
+   `{Closed (omap (maybe BNamed) (f::xl)) e}.
 
 Bind Scope lrust_val_scope with val.
 Delimit Scope lrust_val_scope with RustV.
 
-Definition of_val (v : val) : expr [] :=
+Definition of_val (v : val) : expr :=
   match v with
-  | RecV f x e => Rec f x e
+  | RecV f x e _ => Rec f x e
   | LitV l => Lit l
   end.
 
-Definition to_val (e : expr []) : option val :=
+Definition to_val (e : expr) : option val :=
   match e with
-  | Rec f x e => Some (RecV f x e)
+  | Rec f x e =>
+    match decide _ with
+    | left H => Some (@RecV f x e H)
+    | right _ => None
+    end
   | Lit l => Some (LitV l)
   | _ => None
   end.
@@ -126,22 +114,22 @@ Definition state := gmap loc (lock_state * val).
 
 (** Evaluation contexts *)
 Inductive ectx_item :=
-| BinOpLCtx (op : bin_op) (e2 : expr [])
+| BinOpLCtx (op : bin_op) (e2 : expr)
 | BinOpRCtx (op : bin_op) (v1 : val)
-| AppLCtx (e2 : list (expr []))
-| AppRCtx (v : val) (vl : list val) (el : list (expr []))
+| AppLCtx (e2 : list expr)
+| AppRCtx (v : val) (vl : list val) (el : list expr)
 | ReadCtx (o : order)
-| WriteLCtx (o : order) (e2 : expr [])
+| WriteLCtx (o : order) (e2 : expr)
 | WriteRCtx (o : order) (v1 : val)
-| CasLCtx (e1 e2: expr [])
-| CasMCtx (v0 : val) (e2 : expr [])
+| CasLCtx (e1 e2: expr)
+| CasMCtx (v0 : val) (e2 : expr)
 | CasRCtx (v0 : val) (v1 : val)
 | AllocCtx
-| FreeLCtx (e2 : expr [])
+| FreeLCtx (e2 : expr)
 | FreeRCtx (v1 : val)
-| CaseCtx (el : list (expr [])).
+| CaseCtx (el : list expr).
 
-Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
+Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
   | BinOpLCtx op e2 => BinOp op e e2
   | BinOpRCtx op v1 => BinOp op (of_val v1) e
@@ -160,69 +148,31 @@ Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
   end.
 
 (** Substitution *)
-Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
-  match e return expr Y with
-  | Var x _ => @Var _ x _
-  | Lit l => Lit l
-  | Rec f xl e => Rec f xl (wexpr _ e)
-  | BinOp op e1 e2 => BinOp op (wexpr H e1) (wexpr H e2)
-  | App e el => App (wexpr H e) (map (wexpr H) el)
-  | Read o e => Read o (wexpr H e)
-  | Write o e1 e2 => Write o (wexpr H e1) (wexpr H e2)
-  | CAS e0 e1 e2 => CAS (wexpr H e0) (wexpr H e1) (wexpr H e2)
-  | Alloc e => Alloc (wexpr H e)
-  | Free e1 e2 => Free (wexpr H e1) (wexpr H e2)
-  | Case e el => Case (wexpr H e) (map (wexpr H) el)
-  | Fork e => Fork (wexpr H e)
-  end.
-Solve Obligations with set_solver.
-
-Definition wexpr' {X} (e : expr []) : expr X := wexpr (included_nil _) e.
-
-Definition of_val' {X} (v : val) : expr X := wexpr (included_nil _) (of_val v).
-
-Lemma wsubst_rec_true_prf {X Y x} (H : X `included` x :: Y)
-      {f} {xl : list binder} (Hfxl : BNamed x ≠ f ∧ BNamed x ∉ xl) :
-  xl +b+ f :b: X `included` x :: xl +b+ f :b: Y.
-Proof. set_solver. Qed.
-
-Lemma wsubst_rec_false_prf {X Y x} (H : X `included` x :: Y)
-      {f} {xl : list binder} (Hfxl : ¬ (BNamed x ≠ f ∧ BNamed x ∉ xl)) :
-  xl +b+ f :b: X `included` xl +b+ f :b: Y.
-Proof. move: Hfxl=>/not_and_l [/dec_stable|/dec_stable]; set_solver. Qed.
-
-Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
-    (H : X `included` x :: Y) (e : expr X)  : expr Y :=
-  match e return expr Y with
-  | Var y _ => if decide (x = y) then wexpr' es else @Var _ y _
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | Var y => if decide (x = y) then es else Var y
   | Lit l => Lit l
   | Rec f xl e =>
-     Rec f xl $ match decide (BNamed x ≠ f ∧ BNamed x ∉ xl) return _ with
-                | left Hfy => wsubst x es (wsubst_rec_true_prf H Hfy) e
-                | right Hfy => wexpr (wsubst_rec_false_prf H Hfy) e
-                end
-  | BinOp op e1 e2 => BinOp op (wsubst x es H e1) (wsubst x es H e2)
-  | App e el => App (wsubst x es H e) (map (wsubst x es H) el)
-  | Read o e => Read o (wsubst x es H e)
-  | Write o e1 e2 => Write o (wsubst x es H e1) (wsubst x es H e2)
-  | CAS e0 e1 e2 => CAS (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
-  | Alloc e => Alloc (wsubst x es H e)
-  | Free e1 e2 => Free (wsubst x es H e1) (wsubst x es H e2)
-  | Case e el => Case (wsubst x es H e) (map (wsubst x es H) el)
-  | Fork e => Fork (wsubst x es H e)
+     Rec f xl $
+       if bool_decide (BNamed x ≠ f ∧ BNamed x ∉ xl) then subst x es e else e
+  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
+  | App e el => App (subst x es e) (map (subst x es) el)
+  | Read o e => Read o (subst x es e)
+  | Write o e1 e2 => Write o (subst x es e1) (subst x es e2)
+  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
+  | Alloc e => Alloc (subst x es e)
+  | Free e1 e2 => Free (subst x es e1) (subst x es e2)
+  | Case e el => Case (subst x es e) (map (subst x es) el)
+  | Fork e => Fork (subst x es e)
   end.
-Solve Obligations with set_solver.
-
-Definition subst {X} (x : string) (es : expr []) (e : expr (x :: X)) : expr X :=
-  wsubst x es (λ z, id) e.
-Definition subst' {X} (mx : binder) (es : expr []) : expr (mx :b: X) → expr X :=
-  match mx with BNamed x => subst x es | BAnon => id end.
-Fixpoint subst_l {X} (xl : list binder) (esl : list (expr [])) :
-                     expr (xl +b+ X) → option (expr X) :=
+
+Definition subst' (mx : binder) (es : expr) (e : expr) : expr :=
+  match mx with BNamed x => subst x es e | BAnon => e end.
+Fixpoint subst_l  (xl : list binder) (esl : list expr) (e : expr) : option expr :=
   match xl, esl with
-  | [], [] => λ e, Some e
-  | x::xl, es::esl => λ e, subst_l xl esl (subst' x es e)
-  | _, _ => λ _, None
+  | [], [] => Some e
+  | x::xl, es::esl => subst_l xl esl (subst' x es e)
+  | _, _ => None
   end.
 
 (** The stepping relation *)
@@ -266,11 +216,12 @@ Definition value_eq (σ : state) (v1 v2 : val) : option bool :=
   | _, _ => None
   end.
 
-Inductive head_step : expr [] → state → expr [] → state → option (expr []) → Prop :=
+Inductive head_step : expr → state → expr → state → option expr → Prop :=
 | BinOpS op l1 l2 l' σ :
     bin_op_eval op l1 l2 = Some l' →
     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
 | BetaS f xl e e' el σ:
+    Closed (omap (maybe BNamed) (f::xl)) e →
     Forall (λ ei, is_Some (to_val ei)) el →
     subst_l xl el e = Some e' →
     head_step (App (Rec f xl e) el) σ (subst' f (Rec f xl e) e') σ None
@@ -337,7 +288,7 @@ Inductive head_step : expr [] → state → expr [] → state → option (expr [
     head_step (Fork e) σ (Lit LitUnit) σ (Some e).
 
 (** Atomic expressions *)
-Definition atomic (e: expr []) : bool :=
+Definition atomic (e: expr) : bool :=
   match e with
   | Read (ScOrd | Na2Ord) e | Alloc e => bool_decide (is_Some (to_val e))
   | Write (ScOrd | Na2Ord) e1 e2 | Free e1 e2 =>
@@ -347,95 +298,19 @@ Definition atomic (e: expr []) : bool :=
   | _ => false
   end.
 
-(** Substitution *)
-Lemma var_proof_irrel X x H1 H2 : @Var X x H1 = @Var X x H2.
-Proof. f_equal. by apply (proof_irrel _). Qed.
-
-Lemma wexpr_id X (H : X `included` X) e : wexpr H e = e.
-Proof.
-  revert X H e; fix 3.
-  destruct e as [| | | |? el| | | | | |? el|]; f_equal/=;
-    auto using proof_irrel;
-  induction el; f_equal/=; auto.
-Qed.
-Lemma wexpr_proof_irrel X Y (H1 H2 : X `included` Y) e : wexpr H1 e = wexpr H2 e.
-Proof.
-  revert X Y H1 H2 e; fix 5.
-  destruct e as [| | | |? el| | | | | |? el|]; f_equal/=;
-    auto using proof_irrel;
-  induction el; f_equal/=; auto.
-Qed.
-Lemma wexpr_wexpr X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) H3 e :
-  wexpr H2 (wexpr H1 e) = wexpr H3 e.
-Proof.
-  revert X Y Z H1 H2 H3 e; fix 7.
-  destruct e as [| | | |? el| | | | | |? el|]; f_equal/=;
-    auto using proof_irrel;
-  induction el; f_equal/=; auto.
-Qed.
-Lemma wexpr_wexpr' X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) e :
-  wexpr H2 (wexpr H1 e) = wexpr (transitivity H1 H2) e.
-Proof. apply wexpr_wexpr. Qed.
-
-Lemma wsubst_proof_irrel X Y x es (H1 H2 : X `included` x :: Y) e :
-  wsubst x es H1 e = wsubst x es H2 e.
-Proof.
-  revert X Y H1 H2 e; fix 5.
-  destruct e as [| | | |? el| | | | | |? el|];
-    simpl; intros; try case_decide; f_equal;
-    auto using proof_irrel, wexpr_proof_irrel;
-  induction el; f_equal/=; auto.
-Qed.
-Lemma wexpr_wsubst X Y Z x es (H1: X `included` x::Y) (H2: Y `included` Z) H3 e:
-  wexpr H2 (wsubst x es H1 e) = wsubst x es H3 e.
-Proof.
-  revert X Y Z H1 H2 H3 e; fix 7.
-  destruct e; intros; rewrite /=/wexpr'/=; try case_decide; f_equal; simpl;
-    auto using var_proof_irrel, wexpr_wexpr;
-  induction el; f_equal/=; auto.
-Qed.
-Lemma wsubst_wexpr X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) H3 e:
-  wsubst x es H2 (wexpr H1 e) = wsubst x es H3 e.
-Proof.
-  revert X Y Z H1 H2 H3 e; fix 7.
-  destruct e as [| | | |? el| | | | | |? el|];
-    intros; simpl; try case_decide; f_equal;
-    auto using proof_irrel, wexpr_wexpr;
-  induction el; f_equal/=; auto.
-Qed.
-Lemma wsubst_wexpr' X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) e:
-  wsubst x es H2 (wexpr H1 e) = wsubst x es (transitivity H1 H2) e.
-Proof. apply wsubst_wexpr. Qed.
-
-Lemma wsubst_closed X Y x es (H1 : X `included` x :: Y) H2 (e : expr X) :
-  x ∉ X → wsubst x es H1 e = wexpr H2 e.
-Proof.
-  revert X Y H1 H2 e; fix 5.
-  destruct e as [| | | |? el| | | | | |? el|];
-    intros; rewrite /=/wexpr'/=; try case_decide; f_equal;
-    auto using proof_irrel, wexpr_proof_irrel with set_solver;
-    try (induction el; f_equal/=; auto).
-  clear wsubst_closed. exfalso; set_solver.
-Qed.
-Lemma wsubst_closed_nil x es H (e : expr []) : wsubst x es H e = e.
-Proof.
-  rewrite -{2}(wexpr_id _ (reflexivity []) e).
-  apply wsubst_closed, not_elem_of_nil.
-Qed.
-
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
-Proof. by induction v; simplify_option_eq. Qed.
+Proof.
+  induction v as [|f xl e Hclosed]; first done.
+  cbn [to_val of_val]. destruct decide as [Hclosed'|]; last done.
+  by rewrite !(proof_irrel Hclosed Hclosed').
+Qed.
 
 Lemma of_to_val e v : to_val e = Some v → of_val v = e.
 Proof.
-  revert e v. cut (∀ X (e : expr X) (H : X = ∅) v,
-    to_val (eq_rect _ expr e _ H) = Some v → of_val v = eq_rect _ expr e _ H).
-  { intros help e v. apply (help ∅ e eq_refl). }
-  intros X e; induction e; intros HX ??; simplify_option_eq;
-    repeat match goal with
-    | IH : ∀ _ : ∅ = ∅, _ |- _ => specialize (IH eq_refl); simpl in IH
-    end; auto with f_equal.
+  revert e v. induction e; destruct v; intros [= EQ]; simplify_eq=>//=.
+  - by destruct decide.
+  - by destruct decide; inversion EQ.
 Qed.
 
 Instance of_val_inj : Inj (=) (=) of_val.
@@ -468,7 +343,11 @@ Qed.
 
 Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
   head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
-Proof. destruct Ki; inversion_clear 1; eauto. by decompose_Forall_hyps. Qed.
+Proof.
+  destruct Ki; inversion_clear 1; eauto.
+  - cbn [to_val]. by destruct decide; eauto.
+  - by decompose_Forall_hyps.
+Qed.
 
 Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
   to_val e1 = None → to_val e2 = None →
@@ -532,7 +411,7 @@ Proof. solve_decision. Defined.
 Instance un_op_dec_eq (ord1 ord2 : order) : Decision (ord1 = ord2).
 Proof. solve_decision. Defined.
 
-Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
+Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
   let fix expr_list_beq el el' :=
     match el, el' with
     | [], [] => true
@@ -541,7 +420,7 @@ Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
     end
   in
   match e, e' with
-  | Var x _, Var x' _ => bool_decide (x = x')
+  | Var x, Var x' => bool_decide (x = x')
   | Lit l, Lit l' => bool_decide (l = l')
   | Rec f xl e, Rec f' xl' e' =>
     bool_decide (f = f') && bool_decide (xl = xl') && expr_beq e e'
@@ -558,25 +437,23 @@ Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
   | Free e1 e2, Free e1' e2' => expr_beq e1 e1' && expr_beq e2 e2'
   | _, _ => false
   end.
-Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2 ↔ e1 = e2.
+Lemma expr_beq_correct (e1 e2 : expr) : expr_beq e1 e2 ↔ e1 = e2.
 Proof.
-  revert X e1 e2; fix 2;
+  revert e1 e2; fix 1;
     destruct e1 as [| | | |? el1| | | | | |? el1|],
              e2 as [| | | |? el2| | | | | |? el2|]; simpl; try done;
   rewrite ?andb_True ?bool_decide_spec ?expr_beq_correct;
   try (split; intro; [destruct_and?|split_and?]; congruence).
-  - split; intro. subst. apply var_proof_irrel. congruence.
-  - specialize (expr_beq_correct _ e1). naive_solver.
   - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
     { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
-      specialize (expr_beq_correct _ el1h). naive_solver. }
+      specialize (expr_beq_correct el1h). naive_solver. }
     clear expr_beq_correct. naive_solver.
   - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
     { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
-      specialize (expr_beq_correct _ el1h). naive_solver. }
+      specialize (expr_beq_correct el1h). naive_solver. }
     clear expr_beq_correct. naive_solver.
 Qed.
-Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
+Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
 Proof.
  refine (cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
 Defined.
@@ -585,15 +462,15 @@ Proof.
  refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
 Defined.
 
-Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
+Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
 Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
 
 Canonical Structure stateC := leibnizC state.
 Canonical Structure valC := leibnizC val.
-Canonical Structure exprC X := leibnizC (expr X).
+Canonical Structure exprC := leibnizC expr.
 
 (** Language *)
-Program Instance lrust_ectxi_lang: EctxiLanguage (expr []) val ectx_item state :=
+Program Instance lrust_ectxi_lang: EctxiLanguage expr val ectx_item state :=
   {| ectxi_language.of_val := of_val;
      ectxi_language.to_val := to_val;
      ectxi_language.fill_item := fill_item;
@@ -604,4 +481,4 @@ Solve Obligations with eauto using to_of_val, of_to_val,
   fill_item_val, atomic_fill_item,
   fill_item_no_val_inj, head_ctx_step_val.
 
-Canonical Structure lrust_lang := ectx_lang (expr []).
+Canonical Structure lrust_lang := ectx_lang expr.
diff --git a/lifting.v b/lifting.v
index 54d50a8796d84e29512df19dd46dc04bfc283117..d81de507dbb25daf4f0277bc1b5f65ca9a9efbe9 100644
--- a/lifting.v
+++ b/lifting.v
@@ -10,7 +10,7 @@ Section lifting.
 Context {Σ : iFunctor}.
 Implicit Types P Q : iProp lrust_lang Σ.
 Implicit Types Φ : val → iProp lrust_lang Σ.
-Implicit Types ef : option (expr []).
+Implicit Types ef : option expr.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
@@ -149,14 +149,15 @@ Proof.
   by intros; inv_head_step; eauto. iNext. iFrame. by iApply wp_value.
 Qed.
 
-Lemma wp_rec E f xl erec erec' e el Φ :
-  e = Rec f xl erec →
+Lemma wp_rec E f xl erec `{Closed (omap (maybe BNamed) (f::xl)) erec} erec' el Φ :
   Forall (λ ei, is_Some (to_val ei)) el →
   subst_l xl el erec = Some erec' →
+  let e := Rec f xl erec in
   ▷ WP subst' f e erec' @ E {{ Φ }} ⊢ WP App e el @ E {{ Φ }}.
 Proof.
   iIntros (???) "?". iApply wp_lift_pure_det_head_step; subst; eauto.
-  by intros; inv_head_step; eauto. iNext. by iFrame.
+  - intros; inv_head_step; eauto.
+  - iNext. by iFrame.
 Qed.
 
 Lemma wp_bin_op E op l1 l2 l' Φ :
diff --git a/notation.v b/notation.v
index d98119d238c87059428b553464ef830972d7cbc2..015fd1de606c8a976d4d43ec360bf2c7bf0d7644 100644
--- a/notation.v
+++ b/notation.v
@@ -31,7 +31,6 @@ Notation "# l" := (LitV l%Z%RustV) (at level 8, format "# l").
 Notation "# l" := (Lit l%Z%RustV) (at level 8, format "# l") : lrust_expr_scope.
 
 Notation "' x" := (Var x) (at level 8, format "' x") : lrust_expr_scope.
-Notation "^ e" := (wexpr' e) (at level 8, format "^ e") : lrust_expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
diff --git a/races.v b/races.v
index 088da1945e76b089fd17afcf6253a2c6a83cd7cb..56b2c08ed6061c8b4d384551ccb7025b37c8a3cd 100644
--- a/races.v
+++ b/races.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import gmap.
 Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
 
 Inductive next_access_head :
-  expr [] → state → access_kind * order → loc → Prop :=
+  expr → state → access_kind * order → loc → Prop :=
 | Access_read ord l σ :
     next_access_head (Read ord (Lit $ LitLoc l)) σ (ReadAcc, ord) l
 | Access_write ord l e σ :
@@ -26,10 +26,10 @@ Inductive next_access_head :
                      σ (FreeAcc, Na2Ord) (shift_loc l i).
 
 Definition next_access_thread
-           (e: expr [])(σ : state)  (a : access_kind * order) (l : loc) : Prop :=
+           (e: expr) (σ : state)  (a : access_kind * order) (l : loc) : Prop :=
   ∃ K e', next_access_head e' σ a l ∧ e = fill K e'.
 
-Definition next_accesses_threadpool (el: list (expr [])) (σ : state)
+Definition next_accesses_threadpool (el: list expr) (σ : state)
                                     (a1 a2 : access_kind * order) (l : loc): Prop :=
   ∃ t1 e1 t2 e2 t3, el = t1 ++ e1 :: t2 ++ e2 :: t3 ∧
                     next_access_thread e1 σ a1 l ∧ next_access_thread e2 σ a2 l.
@@ -41,7 +41,7 @@ Definition nonracing_accesses (a1 a2 : access_kind * order) : Prop :=
   | _, _ => False
   end.
 
-Definition nonracing_threadpool (el : list (expr [])) σ : Prop :=
+Definition nonracing_threadpool (el : list expr) σ : Prop :=
   ∀ l a1 a2, next_accesses_threadpool el σ a1 a2 l →
              nonracing_accesses a1 a2.
 
diff --git a/tactics.v b/tactics.v
index 033a9b43ce04c0a6eabaa9f5e5c6fb8f8fb45e09..44bd9ab2b1e9308a3bc91cc5b689b670386fe924 100644
--- a/tactics.v
+++ b/tactics.v
@@ -1,4 +1,4 @@
-From lrust Require Export substitution.
+From lrust Require Export lang.
 From iris.prelude Require Import fin_maps.
 
 (** The tactic [inv_head_step] performs inversion on hypotheses of the
@@ -27,7 +27,6 @@ Ltac reshape_val e tac :=
   let rec go e :=
   match e with
   | of_val ?v => v
-  | wexpr' ?e => reshape_val e tac
   | Lit ?l => constr:(LitV l)
   | Rec ?f ?xl ?e => constr:(RecV f xl e)
   end in let v := go e in first [tac v | fail 2].
@@ -71,5 +70,5 @@ Tactic Notation "do_head_step" tactic3(tac) :=
   | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
      first [apply alloc_fresh|econstructor];
        (* solve [to_val] side-conditions *)
-       first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
+       first [rewrite ?to_of_val; reflexivity|cbn [subst]; tac; fast_done]
   end.
diff --git a/wp_tactics.v b/wp_tactics.v
index faf22a4ae84b2c4146abc96bf11f9170cc08153e..8ffc9998c876f51f7f8dc0b9865a116c25588730 100644
--- a/wp_tactics.v
+++ b/wp_tactics.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export upred_tactics.
-From lrust Require Export tactics derived substitution.
+From lrust Require Export tactics derived.
 Import uPred.
 
 (** wp-specific helper tactics *)
@@ -63,7 +63,7 @@ Tactic Notation "wp_rec" :=
     match eval hnf in e' with App ?e1 _ =>
 (* hnf does not reduce through an of_val *)
 (*      match eval hnf in e1 with Rec _ _ _ => *)
-    wp_bind K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish
+    wp_bind K; etrans; [|eapply wp_rec; wp_done]; cbn [subst]; wp_finish
 (*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
   | _ => fail "wp_rec: not a 'wp'"
   end.
@@ -73,7 +73,7 @@ Tactic Notation "wp_lam" :=
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with App ?e1 _ =>
 (*    match eval hnf in e1 with Rec BAnon _ _ => *)
-    wp_bind K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
+    wp_bind K; etrans; [|eapply wp_lam; wp_done]; cbn [subst]; wp_finish
 (*    end *) end) || fail "wp_lam: cannot find 'Lam' in" e
   | _ => fail "wp_lam: not a 'wp'"
   end.
@@ -109,8 +109,7 @@ Tactic Notation "wp_case" :=
     match eval hnf in e' with
     | Case _ _ _ =>
       wp_bind K;
-      etrans; [|eapply wp_case; wp_done];
-      simpl_subst; wp_finish
+      etrans; [|eapply wp_case; wp_done]; wp_finish
     end) || fail "wp_case: cannot find 'Case' in" e
   | _ => fail "wp_case: not a 'wp'"
   end.