diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index df2041cb291d6e414dbb67aceee9e980286ab466..b59b52772608cb0234aac1082ead17822b1333e0 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -11,6 +11,7 @@ buildjob:
   only:
   - master
   - jh_simplified_resources
+  - rk/substitition
   artifacts:
     paths:
     - build-time.txt
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index 3c8150335c516b2c975230625e30986f6567fa6d..6a96318b218d2a9163cc87b7e5fe67070d29f915 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -19,29 +19,34 @@ Implicit Types Φ : val → iProp heap_lang Σ.
 (** Proof rules for the sugar *)
 Lemma wp_lam E x ef e v Φ :
   to_val e = Some v →
+  Closed (x :b: []) ef →
   ▷ WP subst' x e ef @ E {{ Φ }} ⊢ WP App (Lam x ef) e @ E {{ Φ }}.
 Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
 
 Lemma wp_let E x e1 e2 v Φ :
   to_val e1 = Some v →
+  Closed (x :b: []) e2 →
   ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
 Proof. apply wp_lam. Qed.
 
 Lemma wp_seq E e1 e2 v Φ :
   to_val e1 = Some v →
+  Closed [] e2 →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. intros ?. by rewrite -wp_let. Qed.
+Proof. intros ??. by rewrite -wp_let. Qed.
 
 Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
 Proof. rewrite -wp_seq // -wp_value //. Qed.
 
 Lemma wp_match_inl E e0 v0 x1 e1 x2 e2 Φ :
   to_val e0 = Some v0 →
+  Closed (x1 :b: []) e1 →
   ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
 Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
 
 Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ :
   to_val e0 = Some v0 →
+  Closed (x2 :b: []) e2 →
   ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
 Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed.
 
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index d184fa8fdc0d4d2432f1f888d739e3a0ecbf8712..c1e292fb8d71bc0d842c51ae07b72ed47a4bc56b 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -19,7 +19,6 @@ Inductive bin_op : Set :=
 Inductive binder := BAnon | BNamed : string → binder.
 Delimit Scope binder_scope with bind.
 Bind Scope 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).
@@ -33,27 +32,7 @@ Proof.
   destruct mx; rewrite /= ?elem_of_cons; naive_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) :=
+Inductive expr :=
   (* Base lambda calculus *)
       (* 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
@@ -62,53 +41,75 @@ Inductive expr (X : list string) :=
        * 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}
-  | Rec (f x : binder) (e : expr (f :b: x :b: X))
-  | App (e1 e2 : expr X)
+  | Var (x : string)
+  | Rec (f x : binder) (e : expr)
+  | App (e1 e2 : expr)
   (* Base types and their operations *)
   | Lit (l : base_lit)
-  | UnOp (op : un_op) (e : expr X)
-  | BinOp (op : bin_op) (e1 e2 : expr X)
-  | If (e0 e1 e2 : expr X)
+  | UnOp (op : un_op) (e : expr)
+  | BinOp (op : bin_op) (e1 e2 : expr)
+  | If (e0 e1 e2 : expr)
   (* Products *)
-  | Pair (e1 e2 : expr X)
-  | Fst (e : expr X)
-  | Snd (e : expr X)
+  | Pair (e1 e2 : expr)
+  | Fst (e : expr)
+  | Snd (e : expr)
   (* Sums *)
-  | InjL (e : expr X)
-  | InjR (e : expr X)
-  | Case (e0 : expr X) (e1 : expr X) (e2 : expr X)
+  | InjL (e : expr)
+  | InjR (e : expr)
+  | Case (e0 : expr) (e1 : expr) (e2 : expr)
   (* Concurrency *)
-  | Fork (e : expr X)
+  | Fork (e : expr)
   (* Heap *)
-  | Alloc (e : expr X)
-  | Load (e : expr X)
-  | Store (e1 : expr X) (e2 : expr X)
-  | CAS (e0 : expr X) (e1 : expr X) (e2 : expr X).
+  | Alloc (e : expr)
+  | Load (e : expr)
+  | Store (e1 : expr) (e2 : expr)
+  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
 
 Bind Scope expr_scope with expr.
 Delimit Scope expr_scope with E.
-Arguments Var {_} _ {_}.
-Arguments Rec {_} _ _ _%E.
-Arguments App {_} _%E _%E.
-Arguments Lit {_} _.
-Arguments UnOp {_} _ _%E.
-Arguments BinOp {_} _ _%E _%E.
-Arguments If {_} _%E _%E _%E.
-Arguments Pair {_} _%E _%E.
-Arguments Fst {_} _%E.
-Arguments Snd {_} _%E.
-Arguments InjL {_} _%E.
-Arguments InjR {_} _%E.
-Arguments Case {_} _%E _%E _%E.
-Arguments Fork {_} _%E.
-Arguments Alloc {_} _%E.
-Arguments Load {_} _%E.
-Arguments Store {_} _%E _%E.
-Arguments CAS {_} _%E _%E _%E.
+Arguments Rec _ _ _%E.
+Arguments App _%E _%E.
+Arguments Lit _.
+Arguments UnOp _ _%E.
+Arguments BinOp _ _%E _%E.
+Arguments If _%E _%E _%E.
+Arguments Pair _%E _%E.
+Arguments Fst _%E.
+Arguments Snd _%E.
+Arguments InjL _%E.
+Arguments InjR _%E.
+Arguments Case _%E _%E _%E.
+Arguments Fork _%E.
+Arguments Alloc _%E.
+Arguments Load _%E.
+Arguments Store _%E _%E.
+Arguments CAS _%E _%E _%E.
+
+Fixpoint is_closed (X : list string) (e : expr) : bool :=
+  match e with
+  | Var x => bool_decide (x ∈ X)
+  | Rec f x e => is_closed (f :b: x :b: X) e
+  | Lit _ => true
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
+     is_closed X e
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 =>
+     is_closed X e1 && is_closed X e2
+  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
+     is_closed X e0 && is_closed X e1 && is_closed X e2
+  end.
+
+Section closed.
+  Set Typeclasses Unique Instances.
+  Class Closed (X : list string) (e : expr) := closed : is_closed X e.
+End closed.
+
+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 :=
-  | RecV (f x : binder) (e : expr (f :b: x :b: []))
+  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
   | LitV (l : base_lit)
   | PairV (v1 v2 : val)
   | InjLV (v : val)
@@ -120,18 +121,19 @@ Arguments PairV _%V _%V.
 Arguments InjLV _%V.
 Arguments InjRV _%V.
 
-Fixpoint of_val (v : val) : expr [] :=
+Fixpoint 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
   | PairV v1 v2 => Pair (of_val v1) (of_val v2)
   | InjLV v => InjL (of_val v)
   | InjRV v => InjR (of_val v)
   end.
 
-Fixpoint to_val (e : expr []) : option val :=
+Fixpoint to_val (e : expr) : option val :=
   match e with
-  | Rec f x e => Some (RecV f x e)
+  | Rec f x e =>
+     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
   | Lit l => Some (LitV l)
   | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
   | InjL e => InjLV <$> to_val e
@@ -144,28 +146,28 @@ Definition state := gmap loc val.
 
 (** Evaluation contexts *)
 Inductive ectx_item :=
-  | AppLCtx (e2 : expr [])
+  | AppLCtx (e2 : expr)
   | AppRCtx (v1 : val)
   | UnOpCtx (op : un_op)
-  | BinOpLCtx (op : bin_op) (e2 : expr [])
+  | BinOpLCtx (op : bin_op) (e2 : expr)
   | BinOpRCtx (op : bin_op) (v1 : val)
-  | IfCtx (e1 e2 : expr [])
-  | PairLCtx (e2 : expr [])
+  | IfCtx (e1 e2 : expr)
+  | PairLCtx (e2 : expr)
   | PairRCtx (v1 : val)
   | FstCtx
   | SndCtx
   | InjLCtx
   | InjRCtx
-  | CaseCtx (e1 : expr []) (e2 : expr [])
+  | CaseCtx (e1 : expr) (e2 : expr)
   | AllocCtx
   | LoadCtx
-  | StoreLCtx (e2 : expr [])
+  | StoreLCtx (e2 : expr)
   | StoreRCtx (v1 : val)
-  | CasLCtx (e1 : expr [])  (e2 : expr [])
-  | CasMCtx (v0 : val) (e2 : expr [])
+  | CasLCtx (e1 : expr)  (e2 : expr)
+  | CasMCtx (v0 : val) (e2 : expr)
   | CasRCtx (v0 : val) (v1 : val).
 
-Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
+Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
   | AppLCtx e2 => App e e2
   | AppRCtx v1 => App (of_val v1) e
@@ -182,7 +184,7 @@ Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
   | CaseCtx e1 e2 => Case e e1 e2
   | AllocCtx => Alloc e
   | LoadCtx => Load e
-  | StoreLCtx e2 => Store e e2
+  | StoreLCtx e2 => Store e e2 
   | StoreRCtx v1 => Store (of_val v1) e
   | CasLCtx e1 e2 => CAS e e1 e2
   | CasMCtx v0 e2 => CAS (of_val v0) e e2
@@ -190,79 +192,30 @@ Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
   end.
 
 (** Substitution *)
-(** We have [subst' e BAnon v = e] to deal with anonymous binders *)
-Lemma wexpr_rec_prf {X Y} (H : X `included` Y) {f x} :
-  f :b: x :b: X `included` f :b: x :b: Y.
-Proof. set_solver. Qed.
-
-Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
-  match e return expr Y with
-  | Var x _ => @Var _ x _
-  | Rec f x e => Rec f x (wexpr (wexpr_rec_prf H) e)
-  | App e1 e2 => App (wexpr H e1) (wexpr H e2)
-  | Lit l => Lit l
-  | UnOp op e => UnOp op (wexpr H e)
-  | BinOp op e1 e2 => BinOp op (wexpr H e1) (wexpr H e2)
-  | If e0 e1 e2 => If (wexpr H e0) (wexpr H e1) (wexpr H e2)
-  | Pair e1 e2 => Pair (wexpr H e1) (wexpr H e2)
-  | Fst e => Fst (wexpr H e)
-  | Snd e => Snd (wexpr H e)
-  | InjL e => InjL (wexpr H e)
-  | InjR e => InjR (wexpr H e)
-  | Case e0 e1 e2 => Case (wexpr H e0) (wexpr H e1) (wexpr H e2)
-  | Fork e => Fork (wexpr H e)
-  | Alloc e => Alloc (wexpr H e)
-  | Load  e => Load (wexpr H e)
-  | Store e1 e2 => Store (wexpr H e1) (wexpr H e2)
-  | CAS e0 e1 e2 => CAS (wexpr H e0) (wexpr H e1) (wexpr H e2)
-  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 y}
-    (Hfy : BNamed x ≠ f ∧ BNamed x ≠ y) :
-  f :b: y :b: X `included` x :: f :b: y :b: Y.
-Proof. set_solver. Qed.
-Lemma wsubst_rec_false_prf {X Y x} (H : X `included` x :: Y) {f y}
-    (Hfy : ¬(BNamed x ≠ f ∧ BNamed x ≠ y)) :
-  f :b: y :b: X `included` f :b: y :b: Y.
-Proof. move: Hfy=>/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
   | Rec f y e =>
-     Rec f y $ match decide (BNamed x ≠ f ∧ BNamed x ≠ y) 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
-  | App e1 e2 => App (wsubst x es H e1) (wsubst x es H e2)
+     Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
+  | App e1 e2 => App (subst x es e1) (subst x es e2)
   | Lit l => Lit l
-  | UnOp op e => UnOp op (wsubst x es H e)
-  | BinOp op e1 e2 => BinOp op (wsubst x es H e1) (wsubst x es H e2)
-  | If e0 e1 e2 => If (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
-  | Pair e1 e2 => Pair (wsubst x es H e1) (wsubst x es H e2)
-  | Fst e => Fst (wsubst x es H e)
-  | Snd e => Snd (wsubst x es H e)
-  | InjL e => InjL (wsubst x es H e)
-  | InjR e => InjR (wsubst x es H e)
-  | Case e0 e1 e2 =>
-     Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
-  | Fork e => Fork (wsubst x es H e)
-  | Alloc e => Alloc (wsubst x es H e)
-  | Load e => Load (wsubst x es H e)
-  | Store e1 e2 => Store (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)
+  | UnOp op e => UnOp op (subst x es e)
+  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
+  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
+  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
+  | Fst e => Fst (subst x es e)
+  | Snd e => Snd (subst x es e)
+  | InjL e => InjL (subst x es e)
+  | InjR e => InjR (subst x es e)
+  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
+  | Fork e => Fork (subst x es e)
+  | Alloc e => Alloc (subst x es e)
+  | Load e => Load (subst x es e)
+  | Store e1 e2 => Store (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)
   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 :=
+Definition subst' (mx : binder) (es : expr) : expr → expr :=
   match mx with BNamed x => subst x es | BAnon => id end.
 
 (** The stepping relation *)
@@ -283,9 +236,10 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
   | _, _, _ => None
   end.
 
-Inductive head_step : expr [] → state → expr [] → state → option (expr []) → Prop :=
+Inductive head_step : expr → state → expr → state → option (expr) → Prop :=
   | BetaS f x e1 e2 v2 e' σ :
      to_val e2 = Some v2 →
+     Closed (f :b: x :b: []) e1 →
      e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) →
      head_step (App (Rec f x e1) e2) σ e' σ None
   | UnOpS op l l' σ :
@@ -331,7 +285,7 @@ Inductive head_step : expr [] → state → expr [] → state → option (expr [
      head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
 
 (** Atomic expressions *)
-Definition atomic (e: expr []) : bool :=
+Definition atomic (e: expr) : bool :=
   match e with
   | Alloc e => bool_decide (is_Some (to_val e))
   | Load e => bool_decide (is_Some (to_val e))
@@ -344,76 +298,34 @@ Definition atomic (e: expr []) : bool :=
   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 is_closed_weaken X Y e : is_closed X e → X `included` Y → is_closed Y e.
+Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
 
-Lemma wexpr_id X (H : X `included` X) e : wexpr H e = e.
-Proof. induction e; f_equal/=; auto. by apply (proof_irrel _). Qed.
-Lemma wexpr_proof_irrel X Y (H1 H2 : X `included` Y) e : wexpr H1 e = wexpr H2 e.
+Instance of_val_closed X v : Closed X (of_val v).
 Proof.
-  revert Y H1 H2; induction e; simpl; auto using var_proof_irrel with f_equal.
+  apply is_closed_weaken with []; last set_solver.
+  induction v; simpl; 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 Y Z H1 H2 H3.
-  induction e; simpl; auto using var_proof_irrel with f_equal.
-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 Y H1 H2; induction e; simpl; intros; repeat case_decide;
-    auto using var_proof_irrel, wexpr_proof_irrel with f_equal.
-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.
+Lemma closed_subst X e x es : Closed X e → x ∉ X → subst x es e = e.
 Proof.
-  revert Y Z H1 H2 H3.
-  induction e; intros; repeat (case_decide || simplify_eq/=);
-    unfold wexpr'; auto using var_proof_irrel, wexpr_wexpr with f_equal.
+  rewrite /Closed. revert X.
+  induction e; intros; simpl; try case_decide; f_equal/=; try naive_solver.
+ naive_solver (eauto; set_solver).
 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 Y Z H1 H2 H3.
-  induction e; intros; repeat (case_decide || simplify_eq/=);
-    auto using var_proof_irrel, wexpr_wexpr with f_equal.
-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 Y H1 H2.
-  induction e; intros; repeat (case_decide || simplify_eq/=);
-    auto using var_proof_irrel, wexpr_proof_irrel with f_equal set_solver.
-  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.
+Lemma closed_nil_subst e x es : Closed [] e → subst x es e = e.
+Proof. intros. apply closed_subst with []; set_solver. 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.
+  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
+Qed.
 
 Lemma of_to_val e v : to_val e = Some v → of_val v = e.
 Proof.
-  revert 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 v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
 Qed.
 
 Instance of_val_inj : Inj (=) (=) of_val.
@@ -426,8 +338,7 @@ Lemma fill_item_val Ki e :
   is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
 Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 
-Lemma val_stuck e1 σ1 e2 σ2 ef :
-  head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+Lemma val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
 Lemma atomic_not_val e : atomic e → to_val e = None.
@@ -436,7 +347,7 @@ Proof. by destruct e. Qed.
 Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
 Proof.
   intros. destruct Ki; simplify_eq/=; destruct_and?;
-    repeat (case_match || contradiction); eauto.
+    repeat (simpl || case_match || contradiction); eauto.
 Qed.
 
 Lemma atomic_step e1 σ1 e2 σ2 ef :
@@ -448,7 +359,7 @@ 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; simplify_option_eq; eauto. Qed.
+Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
 
 Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
   to_val e1 = None → to_val e2 = None →
@@ -465,6 +376,77 @@ Lemma alloc_fresh e v σ :
   to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
+(** Value type class *)
+Class Value (e : expr) (v : val) := is_value : to_val e = Some v.
+Instance of_val_value v : Value (of_val v) v.
+Proof. by rewrite /Value to_of_val. Qed.
+Instance rec_value f x e `{!Closed (f :b: x :b: []) e} :
+  Value (Rec f x e) (RecV f x e).
+Proof.
+  rewrite /Value /=; case_decide; last done.
+  do 2 f_equal. by apply (proof_irrel).
+Qed.
+Instance lit_value l : Value (Lit l) (LitV l).
+Proof. done. Qed.
+Instance pair_value e1 e2 v1 v2 :
+  Value e1 v1 → Value e2 v2 → Value (Pair e1 e2) (PairV v1 v2).
+Proof. by rewrite /Value /= => -> /= ->. Qed.
+Instance injl_value e v : Value e v → Value (InjL e) (InjLV v).
+Proof. by rewrite /Value /= => ->. Qed.
+Instance injr_value e v : Value e v → Value (InjR e) (InjRV v).
+Proof. by rewrite /Value /= => ->. Qed.
+
+Section closed_slow.
+  Notation C := Closed.
+
+  Global Instance closed_of_val X v : C X (of_val v).
+  Proof. apply of_val_closed. Qed.
+
+  Lemma closed_var X x : bool_decide (x ∈ X) → C X (Var x).
+  Proof. done. Qed.
+  Global Instance closed_lit X l : C X (Lit l).
+  Proof. done. Qed.
+  Global Instance closed_rec X f x e : C (f :b: x :b: X) e → C X (Rec f x e).
+  Proof. done. Qed.
+  Global Instance closed_unop X op e : C X e → C X (UnOp op e).
+  Proof. done. Qed.
+  Global Instance closed_fst X e : C X e → C X (Fst e).
+  Proof. done. Qed.
+  Global Instance closed_snd X e : C X e → C X (Snd e).
+  Proof. done. Qed.
+  Global Instance closed_injl X e : C X e → C X (InjL e).
+  Proof. done. Qed.
+  Global Instance closed_injr X e : C X e → C X (InjR e).
+  Proof. done. Qed.
+  Global Instance closed_fork X e : C X e → C X (Fork e).
+  Proof. done. Qed.
+  Global Instance closed_load X e : C X e → C X (Load e).
+  Proof. done. Qed.
+  Global Instance closed_alloc X e : C X e → C X (Alloc e).
+  Proof. done. Qed.
+  Global Instance closed_app X e1 e2 : C X e1 → C X e2 → C X (App e1 e2).
+  Proof. intros. by apply andb_True. Qed.
+  Global Instance closed_binop X op e1 e2 : C X e1 → C X e2 → C X (BinOp op e1 e2).
+  Proof. intros. by apply andb_True. Qed.
+  Global Instance closed_pair X e1 e2 : C X e1 → C X e2 → C X (Pair e1 e2).
+  Proof. intros. by apply andb_True. Qed.
+  Global Instance closed_store X e1 e2 : C X e1 → C X e2 → C X (Store e1 e2).
+  Proof. intros. by apply andb_True. Qed.
+  Global Instance closed_if X e0 e1 e2 : C X e0 → C X e1 → C X e2 → C X (If e0 e1 e2).
+  Proof. intros. by rewrite /C /= !andb_True. Qed.
+  Global Instance closed_case X e0 e1 e2 : C X e0 → C X e1 → C X e2 → C X (Case e0 e1 e2).
+  Proof. intros. by rewrite /C /= !andb_True. Qed.
+  Global Instance closed_cas X e0 e1 e2 : C X e0 → C X e1 → C X e2 → C X (CAS e0 e1 e2).
+  Proof. intros. by rewrite /C /= !andb_True. Qed.
+End closed_slow.
+
+Lemma closed_nil_closed X e : Closed [] e → Closed X e.
+Proof. intros. apply is_closed_weaken with []. done. set_solver. Qed.
+Hint Immediate closed_nil_closed : typeclass_instances.
+
+Hint Extern 1000 (Closed _ (Var _)) =>
+  apply closed_var; vm_compute; exact I : typeclass_instances.
+
 (** Equality and other typeclass stuff *)
 Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
 Proof. solve_decision. Defined.
@@ -472,53 +454,25 @@ Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
 Proof. solve_decision. Defined.
 Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
 Proof. solve_decision. Defined.
-
-Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
-  match e, e' with
-  | Var x _, Var x' _ => bool_decide (x = x')
-  | Rec f x e, Rec f' x' e' =>
-     bool_decide (f = f') && bool_decide (x = x') && expr_beq e e'
-  | App e1 e2, App e1' e2' | Pair e1 e2, Pair e1' e2' |
-    Store e1 e2, Store e1' e2' => expr_beq e1 e1' && expr_beq e2 e2'
-  | Lit l, Lit l' => bool_decide (l = l')
-  | UnOp op e, UnOp op' e' => bool_decide (op = op') && expr_beq e e'
-  | BinOp op e1 e2, BinOp op' e1' e2' =>
-     bool_decide (op = op') && expr_beq e1 e1' && expr_beq e2 e2'
-  | If e0 e1 e2, If e0' e1' e2' | Case e0 e1 e2, Case e0' e1' e2' |
-    CAS e0 e1 e2, CAS e0' e1' e2' =>
-     expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2'
-  | Fst e, Fst e' | Snd e, Snd e' | InjL e, InjL e' | InjR e, InjR e' |
-    Fork e, Fork e' | Alloc e, Alloc e' | Load e, Load e' => expr_beq e e'
-  | _, _ => false
-  end.
-Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2 ↔ e1 = e2.
-Proof.
-  split.
-  * revert e2; induction e1; intros [] * ?; simpl in *;
-      destruct_and?; subst; repeat f_equal/=; auto; try apply proof_irrel.
-  * intros ->. induction e2; naive_solver.
-Qed.
-Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
-Proof.
- refine (cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
-Defined.
+Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
+Proof. solve_decision. Defined.
 Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
 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.
 End heap_lang.
 
 (** Language *)
 Program Instance heap_ectxi_lang :
   EctxiLanguage
-    (heap_lang.expr []) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
+    (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
   of_val := heap_lang.of_val; to_val := heap_lang.to_val;
   fill_item := heap_lang.fill_item;
   atomic := heap_lang.atomic; head_step := heap_lang.head_step;
@@ -528,7 +482,7 @@ Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
   heap_lang.fill_item_val, heap_lang.atomic_fill_item,
   heap_lang.fill_item_no_val_inj, heap_lang.head_ctx_step_val.
 
-Canonical Structure heap_lang := ectx_lang (heap_lang.expr []).
+Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
 
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.
diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 236c7aacee4e636614530f0ca3362edd48c37949..68985ead88dafcd8c3fc15e226db0324c7613404 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -1,14 +1,13 @@
 From iris.heap_lang Require Export derived.
 From iris.heap_lang Require Import wp_tactics substitution notation.
 
-Definition Assert {X} (e : expr X) : expr X :=
+Definition Assert (e : expr) : expr :=
   if: e then #() else #0 #0. (* #0 #0 is unsafe *)
 
-Instance do_wexpr_assert {X Y} (H : X `included` Y) e er :
-  WExpr H e er → WExpr H (Assert e) (Assert er) := _.
-Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) e er :
-  WSubst x es H e er → WSubst x es H (Assert e) (Assert er).
-Proof. intros; red. by rewrite /Assert /wsubst -/wsubst; f_equal/=. Qed.
+Instance closed_assert X e : Closed X e → Closed X (Assert e) := _.
+Instance do_subst_assert x es e er :
+  Subst x es e er → Subst x es (Assert e) (Assert er).
+Proof. intros; red. by rewrite /Assert /subst -/subst; f_equal/=. Qed.
 Typeclasses Opaque Assert.
 
 Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) :
diff --git a/heap_lang/lib/barrier/barrier.v b/heap_lang/lib/barrier/barrier.v
index b3b5902ff78e354ed8fb17153283c40c6b3071fa..b9ebaf60b3ffb601d1e1430c81b02760b515d31b 100644
--- a/heap_lang/lib/barrier/barrier.v
+++ b/heap_lang/lib/barrier/barrier.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Export notation.
 
 Definition newbarrier : val := λ: <>, ref #0.
-Definition signal : val := λ: "x", '"x" <- #1.
+Definition signal : val := λ: "x", "x" <- #1.
 Definition wait : val :=
-  rec: "wait" "x" := if: !'"x" = #1 then #() else '"wait" '"x".
+  rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x".
 Global Opaque newbarrier signal wait.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 05d110fbda8ed59d101015df937378328c620688..4940525af7714767b16dce09f53489f4e9f81a0b 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -8,9 +8,9 @@ Import uPred.
 Definition newcounter : val := λ: <>, ref #0.
 Definition inc : val :=
   rec: "inc" "l" :=
-    let: "n" := !'"l" in
-    if: CAS '"l" '"n" (#1 + '"n") then #() else '"inc" '"l".
-Definition read : val := λ: "l", !'"l".
+    let: "n" := !"l" in
+    if: CAS "l" "n" (#1 + "n") then #() else "inc" "l".
+Definition read : val := λ: "l", !"l".
 Global Opaque newcounter inc get.
 
 (** The CMRA we need. *)
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index a5495285cf0ae1e0f9e0b4d515b9601f569b5419..2ce15c16e636b23822bf7f20415795a8d7aaf430 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -6,8 +6,8 @@ Import uPred.
 Definition newlock : val := λ: <>, ref #false.
 Definition acquire : val :=
   rec: "acquire" "l" :=
-    if: CAS '"l" #false #true then #() else '"acquire" '"l".
-Definition release : val := λ: "l", '"l" <- #false.
+    if: CAS "l" #false #true then #() else "acquire" "l".
+Definition release : val := λ: "l", "l" <- #false.
 Global Opaque newlock acquire release.
 
 (** The CMRA we need. *)
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index d1612a5aa7e806217dc7de9da04e8637ead9ca97..15f9ae80b52fe7276aeb17f59f147b6bd36f4997 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -2,18 +2,14 @@ From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
-Definition par {X} : expr X :=
+Definition par : val :=
   λ: "fs",
-    let: "handle" := ^spawn (Fst '"fs") in
-    let: "v2" := Snd '"fs" #() in
-    let: "v1" := ^join '"handle" in
-    Pair '"v1" '"v2".
+    let: "handle" := spawn (Fst "fs") in
+    let: "v2" := Snd "fs" #() in
+    let: "v1" := join "handle" in
+    Pair "v1" "v2".
 Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
 Infix "||" := Par : expr_scope.
-
-Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
-Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
-  WSubst x es H par par := do_wsubst_closed _ x es H _.
 Global Opaque par.
 
 Section proof.
@@ -36,13 +32,14 @@ Proof.
   iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
 Qed.
 
-Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
+Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr) `{!Closed [] e1, Closed [] e2}
+    (Φ : val → iProp) :
   heapN ⊥ N →
   (heap_ctx heapN ★ WP e1 {{ Ψ1 }} ★ WP e2 {{ Ψ2 }} ★
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP e1 || e2 {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); auto.
+  iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); auto. apply is_value.
   iFrame "Hh H". iSplitL "H1"; by wp_let.
 Qed.
 End proof.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index a912a548ec70dfa58bf3153a3587685135d8f69a..00a00b59ee289b8bdcc01b8f800a1626df67516c 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -6,12 +6,12 @@ Import uPred.
 Definition spawn : val :=
   λ: "f",
     let: "c" := ref (InjL #0) in
-    Fork ('"c" <- InjR ('"f" #())) ;; '"c".
+    Fork ("c" <- InjR ("f" #())) ;; "c".
 Definition join : val :=
   rec: "join" "c" :=
-    match: !'"c" with
-      InjR "x" => '"x"
-    | InjL <>  => '"join" '"c"
+    match: !"c" with
+      InjR "x" => "x"
+    | InjL <>  => "join" "c"
     end.
 Global Opaque spawn join.
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index c418dc4f43fe76ed6533c4d8b17b0c1ab4e27a34..709a30a855011ee47159b8dcab9597eb839cb863 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -10,7 +10,7 @@ Section lifting.
 Context {Σ : iFunctor}.
 Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_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 Φ :
@@ -84,9 +84,10 @@ Qed.
 Lemma wp_rec E f x erec e1 e2 v2 Φ :
   e1 = Rec f x erec →
   to_val e2 = Some v2 →
+  Closed (f :b: x :b: []) erec →
   ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
 Proof.
-  intros -> ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
+  intros -> ??. rewrite -(wp_lift_pure_det_head_step (App _ _)
     (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
     intros; inv_head_step; eauto.
 Qed.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 4a33e5a6b7d7841e6c7ebcdf3e843a33eaf8f237..9747dfcdd0a6078608f499d54b665454b57c5e9d 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -24,6 +24,8 @@ Coercion LitLoc : loc >-> base_lit.
 Coercion App : expr >-> Funclass.
 Coercion of_val : val >-> expr.
 
+Coercion Var : string >-> expr.
+
 Coercion BNamed : string >-> binder.
 Notation "<>" := BAnon : binder_scope.
 
@@ -32,9 +34,6 @@ properly. *)
 Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
 Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
 
-Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
-Notation "^ e" := (wexpr' e) (at level 8, format "^ e") : expr_scope.
-
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
 Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 75ea52bef9f13ad4486746b4bac00e28441ba0d6..08cd3b333d26f014eb489367cd4a94c24d131f99 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -2,196 +2,99 @@ From iris.heap_lang Require Export lang.
 Import heap_lang.
 
 (** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
-can be tuned by declaring [WExpr] and [WSubst] instances. *)
-
-(** * Weakening *)
-Class WExpr {X Y} (H : X `included` Y) (e : expr X) (er : expr Y) :=
-  do_wexpr : wexpr H e = er.
-Hint Mode WExpr + + + + - : typeclass_instances.
+can be tuned by declaring [Subst] instances. *)
+(** * Substitution *)
+Class Subst (x : string) (es : expr) (e : expr) (er : expr) :=
+  do_subst : subst x es e = er.
+Hint Mode Subst + + + - : typeclass_instances.
 
 (* Variables *)
-Hint Extern 0 (WExpr _ (Var ?y) _) =>
-  apply var_proof_irrel : typeclass_instances.
-
-(* Rec *)
-Instance do_wexpr_rec_true {X Y f y e} {H : X `included` Y} er :
-  WExpr (wexpr_rec_prf H) e er → WExpr H (Rec f y e) (Rec f y er) | 10.
-Proof. intros; red; f_equal/=. by etrans; [apply wexpr_proof_irrel|]. Qed.
-
-(* Values *)
-Instance do_wexpr_wexpr X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) e er :
-  WExpr (transitivity H1 H2) e er → WExpr H2 (wexpr H1 e) er | 0.
-Proof. by rewrite /WExpr wexpr_wexpr'. Qed.
-Instance do_wexpr_closed_closed (H : [] `included` []) e : WExpr H e e | 1.
-Proof. apply wexpr_id. Qed.
-Instance do_wexpr_closed_wexpr Y (H : [] `included` Y) e :
-  WExpr H e (wexpr' e) | 2.
-Proof. apply wexpr_proof_irrel. Qed.
-
-(* Boring connectives *)
-Section do_wexpr.
-Context {X Y : list string} (H : X `included` Y).
-Notation W := (WExpr H).
-
-(* Ground terms *)
-Global Instance do_wexpr_lit l : W (Lit l) (Lit l).
-Proof. done. Qed.
-Global Instance do_wexpr_app e1 e2 e1r e2r :
-  W e1 e1r → W e2 e2r → W (App e1 e2) (App e1r e2r).
-Proof. intros; red; f_equal/=; apply: do_wexpr. Qed.
-Global Instance do_wexpr_unop op e er : W e er → W (UnOp op e) (UnOp op er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_binop op e1 e2 e1r e2r :
-  W e1 e1r → W e2 e2r → W (BinOp op e1 e2) (BinOp op e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_if e0 e1 e2 e0r e1r e2r :
-  W e0 e0r → W e1 e1r → W e2 e2r → W (If e0 e1 e2) (If e0r e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_pair e1 e2 e1r e2r :
-  W e1 e1r → W e2 e2r → W (Pair e1 e2) (Pair e1r e2r).
-Proof. by intros ??; red; f_equal/=. Qed.
-Global Instance do_wexpr_fst e er : W e er → W (Fst e) (Fst er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_snd e er : W e er → W (Snd e) (Snd er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_injL e er : W e er → W (InjL e) (InjL er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_injR e er : W e er → W (InjR e) (InjR er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_case e0 e1 e2 e0r e1r e2r :
-  W e0 e0r → W e1 e1r → W e2 e2r → W (Case e0 e1 e2) (Case e0r e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_fork e er : W e er → W (Fork e) (Fork er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_alloc e er : W e er → W (Alloc e) (Alloc er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_load e er : W e er → W (Load e) (Load er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_store e1 e2 e1r e2r :
-  W e1 e1r → W e2 e2r → W (Store e1 e2) (Store e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_cas e0 e1 e2 e0r e1r e2r :
-  W e0 e0r → W e1 e1r → W e2 e2r → W (CAS e0 e1 e2) (CAS e0r e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-End do_wexpr.
+Lemma do_subst_var_eq x er : Subst x er (Var x) er.
+Proof. intros; red; simpl. by case_decide. Qed.
+Lemma do_subst_var_neq x y er : bool_decide (x ≠ y) → Subst x er (Var y) (Var y).
+Proof. rewrite bool_decide_spec. intros; red; simpl. by case_decide. Qed.
 
-(** * WSubstitution *)
-Class WSubst {X Y} (x : string) (es : expr []) H (e : expr X) (er : expr Y) :=
-  do_wsubst : wsubst x es H e = er.
-Hint Mode WSubst + + + + + + - : typeclass_instances.
-
-Lemma do_wsubst_closed (e: ∀ {X}, expr X) {X Y} x es (H : X `included` x :: Y) :
-  (∀ X, WExpr (included_nil X) e e) → WSubst x es H e e.
-Proof.
-  rewrite /WSubst /WExpr=> He. rewrite -(He X) wsubst_wexpr'.
-  by rewrite (wsubst_closed _ _ _ _ _ (included_nil _)); last set_solver.
-Qed.
-
-(* Variables *)
-Lemma do_wsubst_var_eq {X Y x es} {H : X `included` x :: Y} `{VarBound x X} er :
-  WExpr (included_nil _) es er → WSubst x es H (Var x) er.
-Proof.
-  intros; red; simpl. case_decide; last done.
-  by etrans; [apply wexpr_proof_irrel|].
-Qed.
-Hint Extern 0 (WSubst ?x ?v _ (Var ?y) _) => first
-  [ apply var_proof_irrel
-  | apply do_wsubst_var_eq ] : typeclass_instances.
+Hint Extern 0 (Subst ?x ?v (Var ?y) _) =>
+  first [apply do_subst_var_eq
+        |apply do_subst_var_neq, I] : typeclass_instances.
 
 (** Rec *)
-Lemma do_wsubst_rec_true {X Y x es f y e} {H : X `included` x :: Y}
-    (Hfy : BNamed x ≠ f ∧ BNamed x ≠ y) er :
-  WSubst x es (wsubst_rec_true_prf H Hfy) e er →
-  WSubst x es H (Rec f y e) (Rec f y er).
-Proof.
-  intros ?; red; f_equal/=; case_decide; last done.
-  by etrans; [apply wsubst_proof_irrel|].
-Qed.
-Lemma do_wsubst_rec_false {X Y x es f y e} {H : X `included` x :: Y}
-    (Hfy : ¬(BNamed x ≠ f ∧ BNamed x ≠ y)) er :
-  WExpr (wsubst_rec_false_prf H Hfy) e er →
-  WSubst x es H (Rec f y e) (Rec f y er).
-Proof.
-  intros; red; f_equal/=; case_decide; first done.
-  by etrans; [apply wexpr_proof_irrel|].
-Qed.
-
-Ltac bool_decide_no_check := apply (bool_decide_unpack _); vm_cast_no_check I.
-Hint Extern 0 (WSubst ?x ?v _ (Rec ?f ?y ?e) _) =>
+Lemma do_subst_rec_true {x es f y e er} :
+  bool_decide (BNamed x ≠ f ∧ BNamed x ≠ y) →
+  Subst x es e er → Subst x es (Rec f y e) (Rec f y er).
+Proof. rewrite bool_decide_spec. intros; red; f_equal/=; by case_decide. Qed.
+Lemma do_subst_rec_false {x es f y e} :
+  bool_decide (¬(BNamed x ≠ f ∧ BNamed x ≠ y)) →
+  Subst x es (Rec f y e) (Rec f y e).
+Proof. rewrite bool_decide_spec. intros; red; f_equal/=; by case_decide. Qed.
+
+Local Ltac bool_decide_no_check := vm_cast_no_check I.
+Hint Extern 0 (Subst ?x ?v (Rec ?f ?y ?e) _) =>
   match eval vm_compute in (bool_decide (BNamed x ≠ f ∧ BNamed x ≠ y)) with
-  | true => eapply (do_wsubst_rec_true ltac:(bool_decide_no_check))
-  | false => eapply (do_wsubst_rec_false ltac:(bool_decide_no_check))
+  | true => eapply (do_subst_rec_true ltac:(bool_decide_no_check))
+  | false => eapply (do_subst_rec_false ltac:(bool_decide_no_check))
   end : typeclass_instances.
 
+Lemma do_subst_closed x es e : Closed [] e → Subst x es e e.
+Proof. apply closed_nil_subst. Qed.
+Hint Extern 10 (Subst ?x ?v ?e _) =>
+  is_var e; class_apply do_subst_closed : typeclass_instances.
+
 (* Values *)
-Instance do_wsubst_wexpr X Y Z x es
-    (H1 : X `included` Y) (H2 : Y `included` x :: Z) e er :
-  WSubst x es (transitivity H1 H2) e er → WSubst x es H2 (wexpr H1 e) er | 0.
-Proof. by rewrite /WSubst wsubst_wexpr'. Qed.
-Instance do_wsubst_closed_closed x es (H : [] `included` [x]) e :
-  WSubst x es H e e | 1.
-Proof. apply wsubst_closed_nil. Qed.
-Instance do_wsubst_closed_wexpr Y x es (H : [] `included` x :: Y) e :
-  WSubst x es H e (wexpr' e) | 2.
-Proof. apply wsubst_closed, not_elem_of_nil. Qed.
+Instance do_subst_of_val x es v : Subst x es (of_val v) (of_val v) | 0.
+Proof. eapply closed_nil_subst, of_val_closed. Qed.
 
 (* Boring connectives *)
-Section wsubst.
-Context {X Y} (x : string) (es : expr []) (H : X `included` x :: Y).
-Notation Sub := (WSubst x es H).
+Section subst.
+Context (x : string) (es : expr).
+Notation Sub := (Subst x es).
 
 (* Ground terms *)
-Global Instance do_wsubst_lit l : Sub (Lit l) (Lit l).
+Global Instance do_subst_lit l : Sub (Lit l) (Lit l).
 Proof. done. Qed.
-Global Instance do_wsubst_app e1 e2 e1r e2r :
+Global Instance do_subst_app e1 e2 e1r e2r :
   Sub e1 e1r → Sub e2 e2r → Sub (App e1 e2) (App e1r e2r).
-Proof. intros; red; f_equal/=; apply: do_wsubst. Qed.
-Global Instance do_wsubst_unop op e er : Sub e er → Sub (UnOp op e) (UnOp op er).
+Proof. intros; red; f_equal/=; apply: do_subst. Qed.
+Global Instance do_subst_unop op e er : Sub e er → Sub (UnOp op e) (UnOp op er).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_binop op e1 e2 e1r e2r :
+Global Instance do_subst_binop op e1 e2 e1r e2r :
   Sub e1 e1r → Sub e2 e2r → Sub (BinOp op e1 e2) (BinOp op e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_if e0 e1 e2 e0r e1r e2r :
+Global Instance do_subst_if e0 e1 e2 e0r e1r e2r :
   Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (If e0 e1 e2) (If e0r e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_pair e1 e2 e1r e2r :
+Global Instance do_subst_pair e1 e2 e1r e2r :
   Sub e1 e1r → Sub e2 e2r → Sub (Pair e1 e2) (Pair e1r e2r).
 Proof. by intros ??; red; f_equal/=. Qed.
-Global Instance do_wsubst_fst e er : Sub e er → Sub (Fst e) (Fst er).
+Global Instance do_subst_fst e er : Sub e er → Sub (Fst e) (Fst er).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_snd e er : Sub e er → Sub (Snd e) (Snd er).
+Global Instance do_subst_snd e er : Sub e er → Sub (Snd e) (Snd er).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_injL e er : Sub e er → Sub (InjL e) (InjL er).
+Global Instance do_subst_injL e er : Sub e er → Sub (InjL e) (InjL er).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_injR e er : Sub e er → Sub (InjR e) (InjR er).
+Global Instance do_subst_injR e er : Sub e er → Sub (InjR e) (InjR er).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_case e0 e1 e2 e0r e1r e2r :
+Global Instance do_subst_case e0 e1 e2 e0r e1r e2r :
   Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (Case e0 e1 e2) (Case e0r e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_fork e er : Sub e er → Sub (Fork e) (Fork er).
+Global Instance do_subst_fork e er : Sub e er → Sub (Fork e) (Fork er).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_alloc e er : Sub e er → Sub (Alloc e) (Alloc er).
+Global Instance do_subst_alloc e er : Sub e er → Sub (Alloc e) (Alloc er).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_load e er : Sub e er → Sub (Load e) (Load er).
+Global Instance do_subst_load e er : Sub e er → Sub (Load e) (Load er).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_store e1 e2 e1r e2r :
+Global Instance do_subst_store e1 e2 e1r e2r :
   Sub e1 e1r → Sub e2 e2r → Sub (Store e1 e2) (Store e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_cas e0 e1 e2 e0r e1r e2r :
+Global Instance do_subst_cas e0 e1 e2 e0r e1r e2r :
   Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (CAS e0 e1 e2) (CAS e0r e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
-End wsubst.
+End subst.
 
 (** * The tactic *)
-Lemma do_subst {X} (x: string) (es: expr []) (e: expr (x :: X)) (er: expr X) :
-  WSubst x es (λ _, id) e er → subst x es e = er.
-Proof. done. Qed.
-
 Ltac simpl_subst :=
   repeat match goal with
-  | |- context [subst ?x ?es ?e] => progress rewrite (@do_subst _ x es e)
+  | |- context [subst ?x ?es ?e] => progress rewrite (@do_subst x es e)
   | |- _ => progress csimpl
   end.
-Arguments wexpr : simpl never.
 Arguments subst : simpl never.
-Arguments wsubst : simpl never.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 4436ec42949735812bd09f2690c24aa10d8455ab..1f669cc2ed5d36b4a0b5d84b1cc651a41daa4c48 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -25,7 +25,6 @@ Ltac reshape_val e tac :=
   let rec go e :=
   match e with
   | of_val ?v => v
-  | wexpr' ?e => go e
   | Rec ?f ?x ?e => constr:(RecV f x e)
   | Lit ?l => constr:(LitV l)
   | Pair ?e1 ?e2 =>
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index d32240a1ddb4b8224e63407669c0d34e16cf50fa..d24924dbaa145beb3ea55358555957e4e20b2755 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -9,7 +9,8 @@ Ltac wp_bind K :=
   | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
 
-Ltac wp_done := rewrite /= ?to_of_val; fast_done.
+(* TODO: Do something better here *)
+Ltac wp_done := fast_done || apply is_value || apply _ || (rewrite /= ?to_of_val; fast_done).
 
 (* sometimes, we will have to do a final view shift, so only apply
 pvs_intro if we obtain a consecutive wp *)
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 268d4a5fa17559ed73753f68abd1b844c7c194f7..482bb97cbf834a1aba4e04b59fe5e98924310359 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -5,12 +5,12 @@ From iris.heap_lang Require Import proofmode.
 Import uPred.
 
 Definition worker (n : Z) : val :=
-  λ: "b" "y", ^wait '"b" ;; !'"y" #n.
-Definition client : expr [] :=
+  λ: "b" "y", wait "b" ;; !"y" #n.
+Definition client : expr :=
   let: "y" := ref #0 in
-  let: "b" := ^newbarrier #() in
-  ('"y" <- (λ: "z", '"z" + #42) ;; ^signal '"b") ||
-    (^(worker 12) '"b" '"y" || ^(worker 17) '"b" '"y").
+  let: "b" := newbarrier #() in
+  ("y" <- (λ: "z", "z" + #42) ;; signal "b") ||
+    (worker 12 "b" "y" || worker 17 "b" "y").
 Global Opaque worker client.
 
 Section client.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index e3dce20dcf60c1e38fdd6405d04102a8bae0fc68..46b0fde18923ac4809560dc8909b7dbdf1a6facb 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -4,13 +4,13 @@ From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
 Section LangTests.
-  Definition add : expr [] := (#21 + #21)%E.
+  Definition add : expr := (#21 + #21)%E.
   Goal ∀ σ, head_step add σ (#42) σ None.
   Proof. intros; do_head_step done. Qed.
-  Definition rec_app : expr [] := ((rec: "f" "x" := '"f" '"x") #0)%E.
+  Definition rec_app : expr := ((rec: "f" "x" := "f" "x") #0)%E.
   Goal ∀ σ, head_step rec_app σ rec_app σ None.
   Proof. intros. rewrite /rec_app. do_head_step done. Qed.
-  Definition lam : expr [] := (λ: "x", '"x" + #21)%E.
+  Definition lam : expr := (λ: "x", "x" + #21)%E.
   Goal ∀ σ, head_step (lam #21)%E σ add σ None.
   Proof. intros. rewrite /lam. do_head_step done. Qed.
 End LangTests.
@@ -21,8 +21,8 @@ Section LiftingTests.
   Implicit Types P Q : iPropG heap_lang Σ.
   Implicit Types Φ : val → iPropG heap_lang Σ.
 
-  Definition heap_e  : expr [] :=
-    let: "x" := ref #1 in '"x" <- !'"x" + #1 ;; !'"x".
+  Definition heap_e  : expr :=
+    let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
   Lemma heap_e_spec E N :
      nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ v, v = #2 }}.
   Proof.
@@ -30,10 +30,10 @@ Section LiftingTests.
     wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
   Qed.
 
-  Definition heap_e2  : expr [] :=
+  Definition heap_e2  : expr :=
     let: "x" := ref #1 in
     let: "y" := ref #1 in
-    '"x" <- !'"x" + #1 ;; !'"x".
+    "x" <- !"x" + #1 ;; !"x".
   Lemma heap_e2_spec E N :
      nclose N ⊆ E → heap_ctx N ⊢ WP heap_e2 @ E {{ v, v = #2 }}.
   Proof.
@@ -44,11 +44,11 @@ Section LiftingTests.
 
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
-      let: "yp" := '"y" + #1 in
-      if: '"yp" < '"x" then '"pred" '"x" '"yp" else '"y".
+      let: "yp" := "y" + #1 in
+      if: "yp" < "x" then "pred" "x" "yp" else "y".
   Definition Pred : val :=
     λ: "x",
-      if: '"x" ≤ #0 then -^FindPred (-'"x" + #2) #0 else ^FindPred '"x" #0.
+      if: "x" ≤ #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
   Global Opaque FindPred Pred.
 
   Lemma FindPred_spec n1 n2 E Φ :
@@ -71,7 +71,7 @@ Section LiftingTests.
   Qed.
 
   Lemma Pred_user E :
-    (True : iProp) ⊢ WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ v, v = #40 }}.
+    (True : iProp) ⊢ WP let: "x" := Pred #42 in Pred "x" @ E {{ v, v = #40 }}.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 5ee3718094ae18cd206ddb108c56eb21703814cb..27316c4ea254d0219166073c153c185023264b3f 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -13,9 +13,9 @@ Definition oneShotGF (F : cFunctor) : gFunctor :=
 Instance inGF_oneShotG  `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F.
 Proof. apply: inGF_inG. Qed.
 
-Definition client eM eW1 eW2 : expr [] :=
+Definition client eM eW1 eW2 : expr :=
   let: "b" := newbarrier #() in
-  (eM ;; ^signal '"b") || ((^wait '"b" ;; eW1) || (^wait '"b" ;; eW2)).
+  (eM ;; signal "b") || ((wait "b" ;; eW1) || (wait "b" ;; eW2)).
 Global Opaque client.
 
 Section proof.
@@ -29,7 +29,7 @@ Definition barrier_res γ (Φ : X → iProp) : iProp :=
   (∃ x, own γ (Cinr $ to_agree $
                Next (cFunctor_map G (iProp_fold, iProp_unfold) x)) ★ Φ x)%I.
 
-Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
+Lemma worker_spec e γ l (Φ Ψ : X → iProp) `{!Closed [] e} :
   recv heapN N l (barrier_res γ Φ) ★ (∀ x, {{ Φ x }} e {{ _, Ψ x }})
   ⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
@@ -64,15 +64,15 @@ Proof.
   iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
 Qed.
 
-Lemma client_spec_new (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) :
-  heapN ⊥ N → eM' = wexpr' eM → eW1' = wexpr' eW1 → eW2' = wexpr' eW2 →
+Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} :
+  heapN ⊥ N →
   heap_ctx heapN ★ P
   ★ {{ P }} eM {{ _, ∃ x, Φ x }}
   ★ (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }})
   ★ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }})
-  ⊢ WP client eM' eW1' eW2' {{ _, ∃ γ, barrier_res γ Ψ }}.
+  ⊢ WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
 Proof.
-  iIntros (HN -> -> ->) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
+  iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
   iPvs (own_alloc (Cinl (Excl ()))) as (γ) "Hγ". done.
   wp_apply (newbarrier_spec heapN N (barrier_res γ Φ)); auto.
   iFrame "Hh". iIntros (l) "[Hr Hs]".
diff --git a/tests/one_shot.v b/tests/one_shot.v
index c77e38b03bb6dc84558cdc97724803cd1b11ca43..c7692fb44ce4ed4992dd2c838b4b66e80946cf6e 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -7,15 +7,15 @@ Import uPred.
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref (InjL #0) in (
   (* tryset *) (λ: "n",
-    CAS '"x" (InjL #0) (InjR '"n")),
+    CAS "x" (InjL #0) (InjR "n")),
   (* check  *) (λ: <>,
-    let: "y" := !'"x" in λ: <>,
-    match: '"y" with
+    let: "y" := !"x" in λ: <>,
+    match: "y" with
       InjL <> => #()
     | InjR "n" =>
-       match: !'"x" with
+       match: !"x" with
          InjL <> => Assert #false
-       | InjR "m" => Assert ('"n" = '"m")
+       | InjR "m" => Assert ("n" = "m")
        end
     end)).
 Global Opaque one_shot_example.