diff --git a/_CoqProject b/_CoqProject
index e587aa9aaa5622b2a0ef7d38a31d2f61e8139e40..497e83782ce1c89c178983a0191e87b2cb2924c6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -81,6 +81,7 @@ theories/program_logic/total_lifting.v
 theories/program_logic/total_ectx_lifting.v
 theories/program_logic/atomic.v
 theories/heap_lang/lang.v
+theories/heap_lang/metatheory.v
 theories/heap_lang/tactics.v
 theories/heap_lang/lifting.v
 theories/heap_lang/notation.v
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index b4ac2c10a5b6822a67b8883062addc91665b61a3..4d17b008c247ad7a2c4644a21ae5b0719b23bb56 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -50,6 +50,18 @@
   --------------------------------------∗
   True
   
+The command has indeed failed with message:
+Ltac call to "wp_pure (open_constr)" failed.
+Tactic failure: wp_pure: cannot find ?y in (Var "x") or 
+?y is not a redex.
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  ============================
+  --------------------------------------∗
+  WP "x" {{ _, True }}
+  
 1 subgoal
   
   Σ : gFunctors
@@ -104,4 +116,4 @@
      : string
 The command has indeed failed with message:
 Ltac call to "wp_cas_suc" failed.
-Tactic failure: wp_cas_suc: cannot find 'CAS' in (#())%E.
+Tactic failure: wp_cas_suc: cannot find 'CAS' in (Val #()).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 922c56acd6435acaf6d914a82eac9c28fe387da2..976695e55b0832ebb22c9aa8736521294b645ce7 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -131,6 +131,10 @@ Section tests.
     WP Alloc #0 {{ _, True }}%I.
   Proof. wp_alloc l as "_". Show. done. Qed.
 
+  Lemma wp_nonclosed_value :
+    WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
+  Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
+
 End tests.
 
 Section printing_tests.
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 179183d14cd686bbed77dae492e17c53db0b7c40..ad39c2b1b3d95f8b7b9f15834ae1366f55531a03 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -82,14 +82,14 @@ Section list_reverse.
     destruct xs as [|x xs]; iSimplifyEq.
     - (* nil *) by wp_match.
     - (* cons *) iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
-      wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
+      wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_pair. wp_store.
       rewrite reverse_cons -assoc.
       iApply ("IH" $! hd' (InjRV #l) xs (x :: ys) with "Hxs [Hx Hys]").
       iExists l, acc; by iFrame.
   Qed.
 
   Lemma rev_ht hd xs :
-    {{ is_list hd xs }} rev hd NONE {{ w, is_list w (reverse xs) }}.
+    {{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
   Proof.
     iIntros "!# Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
     iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
@@ -204,7 +204,7 @@ Section counter_proof.
   Lemma newcounter_spec :
     {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}.
   Proof.
-    iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
     rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
     set (N:= nroot .@ "counter").
@@ -242,7 +242,7 @@ Section counter_proof.
     {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}.
   Proof.
     iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
-    rewrite /read /=. wp_let. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
+    rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
     iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show.
     iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
     { iApply own_op. by iFrame. }
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
index baa2732685cdddb4b868065a8973d881f6dddc52..2c8d900777a7f2ae8771cc1234c9f6b5a14ac975 100644
--- a/tests/list_reverse.ref
+++ b/tests/list_reverse.ref
@@ -23,11 +23,11 @@
   "Hys" : is_list acc ys
   "HΦ" : ∀ w : val, is_list w ys -∗ Φ w
   --------------------------------------∗
-  WP match: InjL #() with
+  WP match: InjLV #() with
        InjL <> => acc
      | InjR "l" =>
        let: "tmp1" := Fst ! "l" in
        let: "tmp2" := Snd ! "l" in
-       "l" <- ("tmp1", acc);; (rev "tmp2") (InjL #())
+       "l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
      end [{ v, Φ v }]
   
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 89b5963bba51711f4faf3223472f10b1c35e5f5f..39d00a1429708b74d24531904c0b4c2e76caff7b 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -36,14 +36,14 @@ Proof.
     iSimplifyEq; wp_rec; wp_let.
   - Show. wp_match. by iApply "HΦ".
   - iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
-    wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
+    wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_pair. wp_store.
     iApply ("IH" $! hd' (SOMEV #l) (x :: ys) with "Hxs [Hx Hys]"); simpl.
     { iExists l, acc; by iFrame. }
     iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
 Qed.
 
 Lemma rev_wp hd xs :
-  [[{ is_list hd xs }]] rev hd NONE [[{ w, RET w; is_list w (reverse xs) }]].
+  [[{ is_list hd xs }]] rev hd NONEV [[{ w, RET w; is_list w (reverse xs) }]].
 Proof.
   iIntros (Φ) "Hxs HΦ".
   iApply (rev_acc_wp hd NONEV xs [] with "[$Hxs //]").
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
index a64d6fb6cb8b67a93f76fc9b6cd42a6ee8490614..08d4ddb27e054a71e9484fbc5f201125f9eeedb5 100644
--- a/tests/one_shot.ref
+++ b/tests/one_shot.ref
@@ -35,7 +35,7 @@
   "Hγ" : own γ (Shot m')
   --------------------------------------∗
   |={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
-               ∗ WP match: InjR #m' with
+               ∗ WP match: InjRV #m' with
                       InjL <> => assert: #false
                     | InjR "m" => assert: #m = "m"
                     end {{ _, True }}
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 79faa4fd39c5d4c55f2f0b1a82d9743133437877..e39d648869feec3499c662cab13e946967d6703c 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -43,12 +43,12 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.
-  rewrite -wp_fupd /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
+  rewrite -wp_fupd /one_shot_example /=. wp_lam. wp_inj. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc Pending) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
-  iModIntro. iApply "Hf"; iSplit.
-  - iIntros (n) "!#". wp_let.
+  wp_closure. wp_closure. wp_pair. iModIntro. iApply "Hf"; iSplit.
+  - iIntros (n) "!#". wp_lam. wp_inj. wp_inj.
     iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
@@ -56,7 +56,7 @@ Proof.
       iModIntro. iNext; iRight; iExists n; by iFrame.
     + wp_cas_fail. iSplitL; last eauto.
       rewrite /one_shot_inv; eauto 10.
-  - iIntros "!# /=". wp_seq. wp_bind (! _)%E.
+  - iIntros "!# /=". wp_lam. wp_bind (! _)%E.
     iInv N as ">Hγ".
     iAssert (∃ v, l ↦ v ∗ ((⌜v = NONEV⌝ ∗ own γ Pending) ∨
        ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv".
@@ -70,7 +70,7 @@ Proof.
       + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     iSplitL "Hinv"; first by eauto.
-    iModIntro. wp_let. iIntros "!#". wp_seq.
+    iModIntro. wp_let. wp_closure. iIntros "!#". wp_lam.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
     { by wp_match. }
     wp_match. wp_bind (! _)%E.
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index 2e91d34175262e978b5d2ceaa04260032fd29f60..b8760ad64f4e854960de890135867c0ae0909d5d 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -58,7 +58,7 @@ Lemma sum_wp `{!heapG Σ} v t :
   [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
 Proof.
   iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
-  wp_let. wp_alloc l as "Hl". wp_let.
+  wp_lam. wp_alloc l as "Hl". wp_let.
   wp_apply (sum_loop_wp with "[$Hl $Ht]").
   rewrite Z.add_0_r.
   iIntros "[Hl Ht]". wp_seq. wp_load. by iApply "HΦ".
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 697a59f78ee1d5843057731dc7ade7088e25fca1..ad5d655d4b5d110aadab4f3951e452df55eaca30 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -59,12 +59,13 @@ Proof.
 Qed.
 
 Inductive expr :=
+  (* Values *)
+  | Val (v : val)
   (* Base lambda calculus *)
   | 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)
   | BinOp (op : bin_op) (e1 e2 : expr)
   | If (e0 e1 e2 : expr)
@@ -86,57 +87,24 @@ Inductive expr :=
   | FAA (e1 : expr) (e2 : expr)
   (* Prophecy *)
   | NewProph
-  | ResolveProph (e1 : expr) (e2 : expr).
-
-Bind Scope expr_scope with expr.
-
-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 _ | NewProph => 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 | FAA e1 e2 | ResolveProph 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.
-
-Class Closed (X : list string) (e : expr) := closed : is_closed X e.
-Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
-Proof. rewrite /Closed. apply _. Qed.
-Instance closed_dec X e : Decision (Closed X e).
-Proof. rewrite /Closed. apply _. Defined.
-
-Inductive val :=
-  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
+  | ResolveProph (e1 : expr) (e2 : expr)
+with val :=
   | LitV (l : base_lit)
+  | RecV (f x : binder) (e : expr)
   | PairV (v1 v2 : val)
   | InjLV (v : val)
   | InjRV (v : val).
 
+Bind Scope expr_scope with expr.
 Bind Scope val_scope with val.
 
 Definition observation : Set := proph_id * val.
 
-Fixpoint of_val (v : val) : expr :=
-  match v with
-  | 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.
+Notation of_val := Val (only parsing).
 
-Fixpoint to_val (e : expr) : option val :=
+Definition to_val (e : expr) : option val :=
   match e with
-  | 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
-  | InjR e => InjRV <$> to_val e
+  | Val v => Some v
   | _ => None
   end.
 
@@ -180,17 +148,13 @@ Record state : Type := {
 
 (** Equality and other typeclass stuff *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
-Proof.
-  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
-Qed.
+Proof. by destruct v. Qed.
 
 Lemma of_to_val e v : to_val e = Some v → of_val v = e.
-Proof.
-  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
-Qed.
+Proof. destruct e=>//=. by intros [= <-]. Qed.
 
 Instance of_val_inj : Inj (=) (=) of_val.
-Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
+Proof. intros ??. congruence. Qed.
 
 Instance base_lit_eq_dec : EqDecision base_lit.
 Proof. solve_decision. Defined.
@@ -199,11 +163,57 @@ Proof. solve_decision. Defined.
 Instance bin_op_eq_dec : EqDecision bin_op.
 Proof. solve_decision. Defined.
 Instance expr_eq_dec : EqDecision expr.
-Proof. solve_decision. Defined.
-Instance val_eq_dec : EqDecision val.
 Proof.
- refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
+  refine (
+   fix go (e1 e2 : expr) {struct e1} : Decision (e1 = e2) :=
+     match e1, e2 with
+     | Val v, Val v' => cast_if (decide (v = v'))
+     | Var x, Var x' => cast_if (decide (x = x'))
+     | Rec f x e, Rec f' x' e' =>
+        cast_if_and3 (decide (f = f')) (decide (x = x')) (decide (e = e'))
+     | App e1 e2, App e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+     | UnOp o e, UnOp o' e' => cast_if_and (decide (o = o')) (decide (e = e'))
+     | BinOp o e1 e2, BinOp o' e1' e2' =>
+        cast_if_and3 (decide (o = o')) (decide (e1 = e1')) (decide (e2 = e2'))
+     | If e0 e1 e2, If e0' e1' e2' =>
+        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
+     | Pair e1 e2, Pair e1' e2' =>
+        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+     | Fst e, Fst e' => cast_if (decide (e = e'))
+     | Snd e, Snd e' => cast_if (decide (e = e'))
+     | InjL e, InjL e' => cast_if (decide (e = e'))
+     | InjR e, InjR e' => cast_if (decide (e = e'))
+     | Case e0 e1 e2, Case e0' e1' e2' =>
+        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
+     | Fork e, Fork e' => cast_if (decide (e = e'))
+     | Alloc e, Alloc e' => cast_if (decide (e = e'))
+     | Load e, Load e' => cast_if (decide (e = e'))
+     | Store e1 e2, Store e1' e2' =>
+        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+     | CAS e0 e1 e2, CAS e0' e1' e2' =>
+        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
+     | FAA e1 e2, FAA e1' e2' =>
+        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+     | NewProph, NewProph => left _
+     | ResolveProph e1 e2, ResolveProph e1' e2' =>
+        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+     | _, _ => right _
+     end
+   with gov (v1 v2 : val) {struct v1} : Decision (v1 = v2) :=
+     match v1, v2 with
+     | LitV l, LitV l' => cast_if (decide (l = l'))
+     | RecV f x e, RecV f' x' e' =>
+        cast_if_and3 (decide (f = f')) (decide (x = x')) (decide (e = e'))
+     | PairV e1 e2, PairV e1' e2' =>
+        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+     | InjLV e, InjLV e' => cast_if (decide (e = e'))
+     | InjRV e, InjRV e' => cast_if (decide (e = e'))
+     | _, _ => right _
+     end
+   for go); try (clear go gov; abstract intuition congruence).
 Defined.
+Instance val_eq_dec : EqDecision val.
+Proof. solve_decision. Defined.
 
 Instance base_lit_countable : Countable base_lit.
 Proof.
@@ -241,64 +251,90 @@ Proof.
 Qed.
 Instance expr_countable : Countable expr.
 Proof.
- set (enc := fix go e :=
-  match e with
-  | Var x => GenLeaf (Some (inl (inl x)))
-  | Rec f x e => GenNode 0 [GenLeaf (Some ((inl (inr f)))); GenLeaf (Some (inl (inr x))); go e]
-  | App e1 e2 => GenNode 1 [go e1; go e2]
-  | Lit l => GenLeaf (Some (inr (inl l)))
-  | UnOp op e => GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); go e]
-  | BinOp op e1 e2 => GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); go e1; go e2]
-  | If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
-  | Pair e1 e2 => GenNode 5 [go e1; go e2]
-  | Fst e => GenNode 6 [go e]
-  | Snd e => GenNode 7 [go e]
-  | InjL e => GenNode 8 [go e]
-  | InjR e => GenNode 9 [go e]
-  | Case e0 e1 e2 => GenNode 10 [go e0; go e1; go e2]
-  | Fork e => GenNode 11 [go e]
-  | Alloc e => GenNode 12 [go e]
-  | Load e => GenNode 13 [go e]
-  | Store e1 e2 => GenNode 14 [go e1; go e2]
-  | CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
-  | FAA e1 e2 => GenNode 16 [go e1; go e2]
-  | NewProph => GenLeaf None
-  | ResolveProph e1 e2 => GenNode 17 [go e1; go e2]
-  end).
- set (dec := fix go e :=
-  match e with
-  | GenLeaf (Some(inl (inl x))) => Var x
-  | GenNode 0 [GenLeaf (Some (inl (inr f))); GenLeaf (Some (inl (inr x))); e] => Rec f x (go e)
-  | GenNode 1 [e1; e2] => App (go e1) (go e2)
-  | GenLeaf (Some (inr (inl l))) => Lit l
-  | GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); e] => UnOp op (go e)
-  | GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); e1; e2] => BinOp op (go e1) (go e2)
-  | GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
-  | GenNode 5 [e1; e2] => Pair (go e1) (go e2)
-  | GenNode 6 [e] => Fst (go e)
-  | GenNode 7 [e] => Snd (go e)
-  | GenNode 8 [e] => InjL (go e)
-  | GenNode 9 [e] => InjR (go e)
-  | GenNode 10 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
-  | GenNode 11 [e] => Fork (go e)
-  | GenNode 12 [e] => Alloc (go e)
-  | GenNode 13 [e] => Load (go e)
-  | GenNode 14 [e1; e2] => Store (go e1) (go e2)
-  | GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
-  | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
-  | GenLeaf None => NewProph
-  | GenNode 17 [e1; e2] => ResolveProph (go e1) (go e2)
-  | _ => Lit LitUnit (* dummy *)
-  end).
- refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
+ set (enc :=
+   fix go e :=
+     match e with
+     | Val v => GenNode 0 [gov v]
+     | Var x => GenLeaf (inl (inl x))
+     | Rec f x e => GenNode 1 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
+     | App e1 e2 => GenNode 2 [go e1; go e2]
+     | UnOp op e => GenNode 3 [GenLeaf (inr (inr (inl op))); go e]
+     | BinOp op e1 e2 => GenNode 4 [GenLeaf (inr (inr (inr op))); go e1; go e2]
+     | If e0 e1 e2 => GenNode 5 [go e0; go e1; go e2]
+     | Pair e1 e2 => GenNode 6 [go e1; go e2]
+     | Fst e => GenNode 7 [go e]
+     | Snd e => GenNode 8 [go e]
+     | InjL e => GenNode 9 [go e]
+     | InjR e => GenNode 10 [go e]
+     | Case e0 e1 e2 => GenNode 11 [go e0; go e1; go e2]
+     | Fork e => GenNode 12 [go e]
+     | Alloc e => GenNode 13 [go e]
+     | Load e => GenNode 14 [go e]
+     | Store e1 e2 => GenNode 15 [go e1; go e2]
+     | CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
+     | FAA e1 e2 => GenNode 17 [go e1; go e2]
+     | NewProph => GenNode 18 []
+     | ResolveProph e1 e2 => GenNode 19 [go e1; go e2]
+     end
+   with gov v :=
+     match v with
+     | LitV l => GenLeaf (inr (inl l))
+     | RecV f x e =>
+        GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
+     | PairV v1 v2 => GenNode 1 [gov v1; gov v2]
+     | InjLV v => GenNode 2 [gov v]
+     | InjRV v => GenNode 3 [gov v]
+     end
+   for go).
+ set (dec :=
+   fix go e :=
+     match e with
+     | GenNode 0 [v] => Val (gov v)
+     | GenLeaf (inl (inl x)) => Var x
+     | GenNode 1 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
+     | GenNode 2 [e1; e2] => App (go e1) (go e2)
+     | GenNode 3 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
+     | GenNode 4 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
+     | GenNode 5 [e0; e1; e2] => If (go e0) (go e1) (go e2)
+     | GenNode 6 [e1; e2] => Pair (go e1) (go e2)
+     | GenNode 7 [e] => Fst (go e)
+     | GenNode 8 [e] => Snd (go e)
+     | GenNode 9 [e] => InjL (go e)
+     | GenNode 10 [e] => InjR (go e)
+     | GenNode 11 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
+     | GenNode 12 [e] => Fork (go e)
+     | GenNode 13 [e] => Alloc (go e)
+     | GenNode 14 [e] => Load (go e)
+     | GenNode 15 [e1; e2] => Store (go e1) (go e2)
+     | GenNode 16 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
+     | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
+     | GenNode 18 [] => NewProph
+     | GenNode 19 [e1; e2] => ResolveProph (go e1) (go e2)
+     | _ => Val $ LitV LitUnit (* dummy *)
+     end
+   with gov v :=
+     match v with
+     | GenLeaf (inr (inl l)) => LitV l
+     | GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => RecV f x (go e)
+     | GenNode 1 [v1; v2] => PairV (gov v1) (gov v2)
+     | GenNode 2 [v] => InjLV (gov v)
+     | GenNode 3 [v] => InjRV (gov v)
+     | _ => LitV LitUnit (* dummy *)
+     end
+   for go).
+ refine (inj_countable' enc dec _).
+ refine (fix go (e : expr) {struct e} := _ with gov (v : val) {struct v} := _ for go).
+ - destruct e as [v| | | | | | | | | | | | | | | | | | | |]; simpl; f_equal;
+     [exact (gov v)|done..].
+ - destruct v; by f_equal.
 Qed.
 Instance val_countable : Countable val.
 Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
 
 Instance state_inhabited : Inhabited state :=
   populate {| heap := inhabitant; used_proph_id := inhabitant |}.
-Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
 Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
+Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
 
 Canonical Structure stateC := leibnizC state.
 Canonical Structure valC := leibnizC val.
@@ -336,10 +372,10 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | AppLCtx v2 => App e (of_val v2)
   | AppRCtx e1 => App e1 e
   | UnOpCtx op => UnOp op e
-  | BinOpLCtx op v2 => BinOp op e (of_val v2)
+  | BinOpLCtx op v2 => BinOp op e (Val v2)
   | BinOpRCtx op e1 => BinOp op e1 e
   | IfCtx e1 e2 => If e e1 e2
-  | PairLCtx v2 => Pair e (of_val v2)
+  | PairLCtx v2 => Pair e (Val v2)
   | PairRCtx e1 => Pair e1 e
   | FstCtx => Fst e
   | SndCtx => Snd e
@@ -348,46 +384,46 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CaseCtx e1 e2 => Case e e1 e2
   | AllocCtx => Alloc e
   | LoadCtx => Load e
-  | StoreLCtx v2 => Store e (of_val v2)
+  | StoreLCtx v2 => Store e (Val v2)
   | StoreRCtx e1 => Store e1 e
-  | CasLCtx v1 v2 => CAS e (of_val v1) (of_val v2)
-  | CasMCtx e0 v2 => CAS e0 e (of_val v2)
+  | CasLCtx v1 v2 => CAS e (Val v1) (Val v2)
+  | CasMCtx e0 v2 => CAS e0 e (Val v2)
   | CasRCtx e0 e1 => CAS e0 e1 e
-  | FaaLCtx v2 => FAA e (of_val v2)
+  | FaaLCtx v2 => FAA e (Val v2)
   | FaaRCtx e1 => FAA e1 e
   | ProphLCtx v2 => ResolveProph e (of_val v2)
   | ProphRCtx e1 => ResolveProph e1 e
   end.
 
 (** Substitution *)
-Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   match e with
-  | Var y => if decide (x = y) then es else Var y
+  | Val _ => e
+  | Var y => if decide (x = y) then Val v else Var y
   | Rec f y e =>
-     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 (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)
-  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
+     Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x v e else e
+  | App e1 e2 => App (subst x v e1) (subst x v e2)
+  | UnOp op e => UnOp op (subst x v e)
+  | BinOp op e1 e2 => BinOp op (subst x v e1) (subst x v e2)
+  | If e0 e1 e2 => If (subst x v e0) (subst x v e1) (subst x v e2)
+  | Pair e1 e2 => Pair (subst x v e1) (subst x v e2)
+  | Fst e => Fst (subst x v e)
+  | Snd e => Snd (subst x v e)
+  | InjL e => InjL (subst x v e)
+  | InjR e => InjR (subst x v e)
+  | Case e0 e1 e2 => Case (subst x v e0) (subst x v e1) (subst x v e2)
+  | Fork e => Fork (subst x v e)
+  | Alloc e => Alloc (subst x v e)
+  | Load e => Load (subst x v e)
+  | Store e1 e2 => Store (subst x v e1) (subst x v e2)
+  | CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
+  | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
   | NewProph => NewProph
-  | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
+  | ResolveProph e1 e2 => ResolveProph (subst x v e1) (subst x v e2)
   end.
 
-Definition subst' (mx : binder) (es : expr) : expr → expr :=
-  match mx with BNamed x => subst x es | BAnon => id end.
+Definition subst' (mx : binder) (v : val) : expr → expr :=
+  match mx with BNamed x => subst x v | BAnon => id end.
 
 (** The stepping relation *)
 Definition un_op_eval (op : un_op) (v : val) : option val :=
@@ -450,82 +486,82 @@ Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: sta
 Arguments state_upd_used_proph_id _ !_ /.
 
 Inductive head_step : expr → state → list observation → expr → state → list (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' σ []
-  | UnOpS op e v v' σ :
-     to_val e = Some v →
+  | RecS f x e σ :
+     head_step (Rec f x e) σ [] (Val $ RecV f x e) σ []
+  | PairS v1 v2 σ :
+     head_step (Pair (Val v1) (Val v2)) σ [] (Val $ PairV v1 v2) σ []
+  | InjLS v σ :
+     head_step (InjL $ Val v) σ [] (Val $ InjLV v) σ []
+  | InjRS v σ :
+     head_step (InjR $ Val v) σ [] (Val $ InjRV v) σ []
+  | BetaS f x e1 v2 e' σ :
+     e' = subst' x v2 (subst' f (RecV f x e1) e1) →
+     head_step (App (Val $ RecV f x e1) (Val v2)) σ [] e' σ []
+  | UnOpS op v v' σ :
      un_op_eval op v = Some v' →
-     head_step (UnOp op e) σ [] (of_val v') σ []
-  | BinOpS op e1 e2 v1 v2 v' σ :
-     to_val e1 = Some v1 → to_val e2 = Some v2 →
+     head_step (UnOp op (Val v)) σ [] (Val v') σ []
+  | BinOpS op v1 v2 v' σ :
      bin_op_eval op v1 v2 = Some v' →
-     head_step (BinOp op e1 e2) σ [] (of_val v') σ []
+     head_step (BinOp op (Val v1) (Val v2)) σ [] (Val v') σ []
   | IfTrueS e1 e2 σ :
-     head_step (If (Lit $ LitBool true) e1 e2) σ [] e1 σ []
+     head_step (If (Val $ LitV $ LitBool true) e1 e2) σ [] e1 σ []
   | IfFalseS e1 e2 σ :
-     head_step (If (Lit $ LitBool false) e1 e2) σ [] e2 σ []
-  | FstS e1 v1 e2 v2 σ :
-     to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Fst (Pair e1 e2)) σ [] e1 σ []
-  | SndS e1 v1 e2 v2 σ :
-     to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Snd (Pair e1 e2)) σ [] e2 σ []
-  | CaseLS e0 v0 e1 e2 σ :
-     to_val e0 = Some v0 →
-     head_step (Case (InjL e0) e1 e2) σ [] (App e1 e0) σ []
-  | CaseRS e0 v0 e1 e2 σ :
-     to_val e0 = Some v0 →
-     head_step (Case (InjR e0) e1 e2) σ [] (App e2 e0) σ []
+     head_step (If (Val $ LitV $ LitBool false) e1 e2) σ [] e2 σ []
+  | FstS v1 v2 σ :
+     head_step (Fst (Val $ PairV v1 v2)) σ [] (Val v1) σ []
+  | SndS v1 v2 σ :
+     head_step (Snd (Val $ PairV v1 v2)) σ [] (Val v2) σ []
+  | CaseLS v e1 e2 σ :
+     head_step (Case (Val $ InjLV v) e1 e2) σ [] (App e1 (Val v)) σ []
+  | CaseRS v e1 e2 σ :
+     head_step (Case (Val $ InjRV v) e1 e2) σ [] (App e2 (Val v)) σ []
   | ForkS e σ:
-     head_step (Fork e) σ [] (Lit LitUnit) σ [e]
-  | AllocS e v σ l :
-     to_val e = Some v → σ.(heap) !! l = None →
-     head_step (Alloc e) σ
+     head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
+  | AllocS v σ l :
+     σ.(heap) !! l = None →
+     head_step (Alloc $ Val v) σ
                []
-               (Lit $ LitLoc l) (state_upd_heap <[l:=v]> σ)
+               (Val $ LitV $ LitLoc l) (state_upd_heap <[l:=v]> σ)
                []
   | LoadS l v σ :
      σ.(heap) !! l = Some v →
-     head_step (Load (Lit $ LitLoc l)) σ [] (of_val v) σ []
-  | StoreS l e v σ :
-     to_val e = Some v → is_Some (σ.(heap) !! l) →
-     head_step (Store (Lit $ LitLoc l) e) σ
+     head_step (Load (Val $ LitV $ LitLoc l)) σ [] (of_val v) σ []
+  | StoreS l v σ :
+     is_Some (σ.(heap) !! l) →
+     head_step (Store (Val $ LitV $ LitLoc l) (Val v)) σ
                []
-               (Lit LitUnit) (state_upd_heap <[l:=v]> σ)
+               (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
                []
-  | CasFailS l e1 v1 e2 v2 vl σ :
-     to_val e1 = Some v1 → to_val e2 = Some v2 →
+  | CasFailS l v1 v2 vl σ :
      σ.(heap) !! l = Some vl → vl ≠ v1 →
      vals_cas_compare_safe vl v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ LitBool false) σ []
-  | CasSucS l e1 v1 e2 v2 σ :
-     to_val e1 = Some v1 → to_val e2 = Some v2 →
+     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ []
+               (Val $ LitV $ LitBool false) σ []
+  | CasSucS l v1 v2 σ :
      σ.(heap) !! l = Some v1 →
      vals_cas_compare_safe v1 v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ
+     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
                []
-               (Lit $ LitBool true) (state_upd_heap <[l:=v2]> σ)
+               (Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ)
                []
-  | FaaS l i1 e2 i2 σ :
-     to_val e2 = Some (LitV (LitInt i2)) →
+  | FaaS l i1 i2 σ :
      σ.(heap) !! l = Some (LitV (LitInt i1)) →
-     head_step (FAA (Lit $ LitLoc l) e2) σ
+     head_step (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ
                []
-               (Lit $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]> σ)
+               (Val $ LitV $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]>σ)
                []
   | NewProphS σ p :
      p ∉ σ.(used_proph_id) →
      head_step NewProph σ
                []
-               (Lit $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ)
+               (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ)
                []
   | ResolveProphS e1 p e2 v σ :
      to_val e1 = Some (LitV $ LitProphecy p) →
      to_val e2 = Some v →
-     head_step (ResolveProph e1 e2) σ [(p, v)] (Lit LitUnit) σ [].
+     head_step (ResolveProph (Val $ LitV $ LitProphecy p) (Val v)) σ
+               [(p, v)]
+               (Val $ LitV LitUnit) σ [].
 
 (** Basic properties about the language *)
 Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
@@ -545,96 +581,18 @@ 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 →
   fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
-Proof.
-  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
-    repeat match goal with
-    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
-    end; auto.
-Qed.
+Proof. destruct Ki1, Ki2; intros; by simplify_eq. Qed.
 
-Lemma alloc_fresh e v σ :
+Lemma alloc_fresh v σ :
   let l := fresh (dom (gset loc) σ.(heap)) in
-  to_val e = Some v →
-  head_step (Alloc e) σ [] (Lit (LitLoc l)) (state_upd_heap <[l:=v]> σ) [].
+  head_step (Alloc $ Val v) σ [] (Val $ LitV $ LitLoc l) (state_upd_heap <[l:=v]> σ) [].
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
 
 Lemma new_proph_id_fresh σ :
   let p := fresh σ.(used_proph_id) in
-  head_step NewProph σ [] (Lit $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ) [].
+  head_step NewProph σ [] (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ) [].
 Proof. constructor. apply is_fresh. Qed.
 
-(* Misc *)
-Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :
-  to_val (Rec f x e) = Some (RecV f x e).
-Proof. rewrite /to_val. case_decide=> //. do 2 f_equal; apply proof_irrel. Qed.
-
-(** Closed expressions *)
-Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
-Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
-
-Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
-Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
-
-Lemma is_closed_of_val X v : is_closed X (of_val v).
-Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
-
-Lemma is_closed_to_val X e v : to_val e = Some v → is_closed X e.
-Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
-
-Lemma is_closed_subst X e x es :
-  is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).
-Proof.
-  intros ?. revert X.
-  induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
-    try match goal with
-    | H : ¬(_ ∧ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
-    end; eauto using is_closed_weaken with set_solver.
-Qed.
-Lemma is_closed_do_subst' X e x es :
-  is_closed [] es → is_closed (x :b: X) e → is_closed X (subst' x es e).
-Proof. destruct x; eauto using is_closed_subst. Qed.
-
-(* Substitution *)
-Lemma subst_is_closed X e x es : is_closed X e → x ∉ X → subst x es e = e.
-Proof.
-  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
-    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
-Qed.
-
-Lemma subst_is_closed_nil e x es : is_closed [] e → subst x es e = e.
-Proof. intros. apply subst_is_closed with []; set_solver. Qed.
-
-Lemma subst_subst e x es es' :
-  Closed [] es' → subst x es (subst x es' e) = subst x es' e.
-Proof.
-  intros. induction e; simpl; try (f_equal; by auto);
-    simplify_option_eq; auto using subst_is_closed_nil with f_equal.
-Qed.
-Lemma subst_subst' e x es es' :
-  Closed [] es' → subst' x es (subst' x es' e) = subst' x es' e.
-Proof. destruct x; simpl; auto using subst_subst. Qed.
-
-Lemma subst_subst_ne e x y es es' :
-  Closed [] es → Closed [] es' → x ≠ y →
-  subst x es (subst y es' e) = subst y es' (subst x es e).
-Proof.
-  intros. induction e; simpl; try (f_equal; by auto);
-    simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
-Qed.
-Lemma subst_subst_ne' e x y es es' :
-  Closed [] es → Closed [] es' → x ≠ y →
-  subst' x es (subst' y es' e) = subst' y es' (subst' x es e).
-Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.
-
-Lemma subst_rec' f y e x es :
-  x = f ∨ x = y ∨ x = BAnon →
-  subst' x es (Rec f y e) = Rec f y e.
-Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
-Lemma subst_rec_ne' f y e x es :
-  (x ≠ f ∨ f = BAnon) → (x ≠ y ∨ y = BAnon) →
-  subst' x es (Rec f y e) = Rec f y (subst' x es e).
-Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
-
 Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
 Proof.
   split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
@@ -659,4 +617,6 @@ Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
 Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
 Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
 
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
+(* Skip should be atomic, we sometimes open invariants around
+   it. Hence, we need to explicitly use LamV instead of e.g., Seq. *)
+Notation Skip := (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUnit)).
diff --git a/theories/heap_lang/lib/assert.v b/theories/heap_lang/lib/assert.v
index ce10822a07640763dedaa3c9e61b88f705015d9f..4a7733f14beb21f029d82689751d396f89b1a2ea 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -9,16 +9,16 @@ Definition assert : val :=
 (* just below ;; *)
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 
-Lemma twp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
+Lemma twp_assert `{heapG Σ} E (Φ : val → iProp Σ) e :
   WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗ WP assert: e @ E [{ Φ }].
 Proof.
-  iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
+  iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
   wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
 
-Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
+Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
 Proof.
-  iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
+  iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
   wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index 22adb5813992abb129a9b42e549fa4e4dd4810d5..c88ba0204173197176eec74c2ba60805ad40733c 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -21,21 +21,20 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
     AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
   mapsto_agree l q1 q2 v1 v2 :> mapsto l q1 v1 -∗ mapsto l q2 v2 -∗ ⌜v1 = v2⌝;
   (* -- operation specs -- *)
-  alloc_spec e v :
-    IntoVal e v → {{{ True }}} alloc e {{{ l, RET #l; mapsto l 1 v }}};
+  alloc_spec (v : val) :
+    {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
   load_spec (l : loc) :
     <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
-  store_spec (l : loc) (e : expr) (w : val) :
-    IntoVal e w →
-    <<< ∀ v, mapsto l 1 v >>> store #l e @ ⊤
+  store_spec (l : loc) (w : val) :
+    <<< ∀ v, mapsto l 1 v >>> store #l w @ ⊤
     <<< mapsto l 1 w, RET #() >>>;
   (* This spec is slightly weaker than it could be: It is sufficient for [w1]
   *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
   is outside the atomic triple, which makes it much easier to use -- and the
   spec is still good enough for all our applications. *)
-  cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
-    IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
-    <<< ∀ v, mapsto l 1 v >>> cas #l e1 e2 @ ⊤
+  cas_spec (l : loc) (w1 w2 : val) :
+    val_is_unboxed w1 →
+    <<< ∀ v, mapsto l 1 v >>> cas #l w1 w2 @ ⊤
     <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
         RET #(if decide (v = w1) then true else false) >>>;
 }.
@@ -72,39 +71,38 @@ Definition primitive_cas : val :=
 Section proof.
   Context `{!heapG Σ}.
 
-  Lemma primitive_alloc_spec e v :
-    IntoVal e v → {{{ True }}} primitive_alloc e {{{ l, RET #l; l ↦ v }}}.
+  Lemma primitive_alloc_spec (v : val) :
+    {{{ True }}} primitive_alloc v {{{ l, RET #l; l ↦ v }}}.
   Proof.
-    iIntros (<- Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done.
+    iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l. iApply "HΦ". done.
   Qed.
 
   Lemma primitive_load_spec (l : loc) :
     <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
     <<< l ↦{q} v, RET v >>>.
   Proof.
-    iIntros (Q Φ) "? AU". wp_let.
+    iIntros (Q Φ) "? AU". wp_lam.
     iMod "AU" as (v q) "[H↦ [_ Hclose]]".
     wp_load. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
 
-  Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
-    IntoVal e w →
-    <<< ∀ v, l ↦ v >>> primitive_store #l e @ ⊤
+  Lemma primitive_store_spec (l : loc) (w : val) :
+    <<< ∀ v, l ↦ v >>> primitive_store #l w @ ⊤
     <<< l ↦ w, RET #() >>>.
   Proof.
-    iIntros (<- Q Φ) "? AU". wp_lam. wp_let.
+    iIntros (Q Φ) "? AU". wp_lam. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
     wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
 
-  Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
-    IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
+  Lemma primitive_cas_spec (l : loc) (w1 w2 : val) :
+    val_is_unboxed w1 →
     <<< ∀ (v : val), l ↦ v >>>
-      primitive_cas #l e1 e2 @ ⊤
+      primitive_cas #l w1 w2 @ ⊤
     <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
         RET #(if decide (v = w1) then true else false) >>>.
   Proof.
-    iIntros (<- <- ? Q Φ) "? AU". wp_lam. wp_let. wp_let.
+    iIntros (? Q Φ) "? AU". wp_lam. wp_let. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
     destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
     iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index 65d05ea26037cb53c72016e9bb81ed0b90e55315..5647d1c2dd4f9722728aac726f31a3b82835d63f 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -36,12 +36,11 @@ Section coinflip.
   Lemma rand_spec :
     {{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
   Proof.
-    iIntros (Φ) "_ HP".
-    wp_lam. wp_alloc l as "Hl". wp_lam.
+    iIntros (Φ) "_ HP". wp_lam. wp_alloc l as "Hl". wp_let.
     iMod (inv_alloc N _ (∃ (b: bool), l ↦ #b)%I with "[Hl]") as "#Hinv"; first by eauto.
     wp_apply wp_fork.
     - iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
-    - wp_lam. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
+    - wp_seq. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
       iApply "HP". done.
   Qed.
 
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 788eb85800e92526c9ea674b08cfee97001306fc..6ab8cbe5bddd0aa442aa0ad51c46d20c72fb8cf5 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -35,7 +35,7 @@ Section mono_proof.
   Lemma newcounter_mono_spec :
     {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
@@ -71,7 +71,7 @@ Section mono_proof.
     {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}.
   Proof.
     iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
-    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]".
+    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
     wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
       as %[?%mnat_included _]%auth_valid_discrete_2.
@@ -112,7 +112,7 @@ Section contrib_spec.
     {{{ True }}} newcounter #()
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
@@ -144,7 +144,7 @@ Section contrib_spec.
     {{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
-    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
+    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
@@ -155,7 +155,7 @@ Section contrib_spec.
     {{{ n, RET #n; ccounter γ 1 n }}}.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
-    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
+    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     by iApply "HΦ".
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index d26b432921e628ef895f04b0e8e2ae8fcea62bdb..c6a3a92f2c8f82f264d263e42ee761cd04b1bf08 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -23,15 +23,14 @@ Section increment.
   Lemma incr_spec (l: loc) :
     <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_let.
+    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_apply load_spec; first by iAccu.
     (* Prove the atomic update for load *)
     iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
     iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
     iIntros "$ !> AU !> _".
     (* Now go on *)
-    wp_let. wp_op. wp_bind (CAS _ _ _)%I.
-    wp_apply cas_spec; [done|iAccu|].
+    wp_let. wp_op. wp_apply cas_spec; [done|iAccu|].
     (* Prove the atomic update for CAS *)
     iAuIntro. iApply (aacc_aupd with "AU"); first done.
     iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
@@ -57,7 +56,7 @@ Section increment.
       weak_incr #l @ ⊤
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_let.
+    iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
     wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
     iIntros "Hl". wp_let. wp_op.
     wp_apply store_spec; first by iAccu.
@@ -86,7 +85,7 @@ Section increment_client.
   Lemma incr_client_safe (x: Z):
     WP incr_client #x {{ _, True }}%I.
   Proof using Type*.
-    wp_let. wp_alloc l as "Hl". wp_let.
+    wp_lam. wp_alloc l as "Hl". wp_let.
     iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto.
     (* FIXME: I am only using persistent stuff, so I should be allowed
        to move this to the persisten context even without the additional â–¡. *)
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index eaf7d05cb6ac5e2b1ef327b887238573bed16a1e..4691dfefc1f6bb43d0352fa0b8dbc5676e137801 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -6,12 +6,12 @@ Import uPred.
 Definition parN : namespace := nroot .@ "par".
 
 Definition par : val :=
-  λ: "fs",
-    let: "handle" := spawn (Fst "fs") in
-    let: "v2" := Snd "fs" #() in
+  λ: "e1" "e2",
+    let: "handle" := spawn "e1" in
+    let: "v2" := "e2" #() in
     let: "v1" := join "handle" in
     ("v1", "v2").
-Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
+Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
 
 Section proof.
 Local Set Default Proof Using "Type*".
@@ -21,28 +21,26 @@ Context `{!heapG Σ, !spawnG Σ}.
    brought together.  That is strictly stronger than first stripping a later
    and then merging them, as demonstrated by [tests/joining_existentials.v].
    This is why these are not Texan triples. *)
-Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) :
-  IntoVal e (f1,f2) →
+Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) (f1 f2 : val) (Φ : val → iProp Σ) :
   WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗
   (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
-  WP par e {{ Φ }}.
+  WP par f1 f2 {{ Φ }}.
 Proof.
-  iIntros (<-) "Hf1 Hf2 HΦ".
-  rewrite /par /=. wp_let. wp_proj.
+  iIntros "Hf1 Hf2 HΦ".
+  rewrite /par /=. wp_lam. wp_let.
   wp_apply (spawn_spec parN with "Hf1").
-  iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
-  iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
+  iIntros (l) "Hl". wp_let. wp_bind (f2 _).
+  wp_apply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
   wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
-  iSpecialize ("HΦ" with "[-]"); first by iSplitL "H1". by wp_let.
+  iSpecialize ("HΦ" with "[-]"); first by iSplitL "H1". wp_let. by wp_pair.
 Qed.
 
-Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ)
-    (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val → iProp Σ) :
+Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :
   WP e1 {{ Ψ1 }} -∗ WP e2 {{ Ψ2 }} -∗
   (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
   WP e1 ||| e2 {{ Φ }}.
 Proof.
-  iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]").
-  by wp_let. by wp_let. auto.
+  iIntros "H1 H2 H". do 2 wp_closure.
+  iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
 Qed.
 End proof.
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index acd4f0a8c6c7acc9caa29466a21f6163c867c057..900f75786db8efe6784772a435c647bf4d11e915 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -49,13 +49,13 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
   {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
 Proof.
   iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
-  wp_let. wp_alloc l as "Hl". wp_let.
+  wp_lam. wp_inj. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
   { iNext. iExists NONEV. iFrame; eauto. }
   wp_apply (wp_fork with "[Hf]").
   - iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
-    iInv N as (v') "[Hl _]".
+    wp_inj. iInv N as (v') "[Hl _]".
     wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
   - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
 Qed.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index f3cf0e07244a3b1512166dab528cd144a3cd31dd..5b010185c020dba618f23713ae646fbfd00e15f7 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -83,7 +83,7 @@ Section proof.
   Proof.
     iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
     iDestruct "Hlock" as (l ->) "#Hinv".
-    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]".
+    rewrite /release /=. wp_lam. iInv N as (b) "[Hl _]".
     wp_store. iSplitR "HΦ"; last by iApply "HΦ".
     iModIntro. iNext. iExists false. by iFrame.
   Qed.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index caf6ff093616c6d3bbace6a27ccc3d0502f88410..2da04f5786cae2c07388c6706ad3d0239ac6a041 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -73,14 +73,14 @@ Section proof.
   Lemma newlock_spec (R : iProp Σ) :
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
-    wp_seq. wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
+    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=. repeat wp_proj.
+    wp_lam. wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
     iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
     { by rewrite -auth_both_op. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
       iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
-    iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
+    wp_pair. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
   Qed.
 
   Lemma wait_loop_spec γ lk x R :
@@ -137,7 +137,7 @@ Section proof.
   Proof.
     iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
     iDestruct "Hγ" as (o) "Hγo".
-    wp_let. wp_proj. wp_bind (! _)%E.
+    wp_lam. wp_proj. wp_bind (! _)%E.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
     wp_load.
     iDestruct (own_valid_2 with "Hauth Hγo") as
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index b7805d0789605ab20537acb69aaf2055b6974943..fe203669c01896dbcae26ad9606a4a7194df210d 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -44,7 +44,6 @@ Ltac inv_head_step :=
      inversion H; subst; clear H
   end.
 
-Local Hint Extern 0 (atomic _ _) => solve_atomic.
 Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
 Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl.
 
@@ -59,51 +58,61 @@ Local Hint Resolve to_of_val.
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
-  unfold IntoVal in *;
-  repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
-  intros ?; apply nsteps_once, pure_head_step_pure_step;
+  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
     constructor; [solve_exec_safe | solve_exec_puredet].
 
-Class AsRec (e : expr) (f x : binder) (erec : expr) :=
-  as_rec : e = Rec f x erec.
-Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
-Instance AsRec_rec_locked_val v f x e :
-  AsRec (of_val v) f x e → AsRec (of_val (locked v)) f x e.
+Class AsRecV (v : val) (f x : binder) (erec : expr) :=
+  as_recv : v = RecV f x erec.
+Instance AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
+Instance AsRecV_recv_locked v f x e :
+  AsRecV v f x e → AsRecV (locked v) f x e.
 Proof. by unlock. Qed.
 
-Instance pure_rec f x (erec e1 e2 : expr)
-    `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
-  PureExec True 1 (App e1 e2) (subst' x e2 (subst' f e1 erec)).
-Proof. unfold AsRec in *; solve_pure_exec. Qed.
+Instance pure_recc f x (erec : expr) :
+  PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
+Proof. solve_pure_exec. Qed.
+Instance pure_pairc (v1 v2 : val) :
+  PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
+Proof. solve_pure_exec. Qed.
+Instance pure_injlc (v : val) :
+  PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
+Proof. solve_pure_exec. Qed.
+Instance pure_injrc (v : val) :
+  PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
+Proof. solve_pure_exec. Qed.
 
-Instance pure_unop op e v v' `{!IntoVal e v} :
-  PureExec (un_op_eval op v = Some v') 1 (UnOp op e) (of_val v').
+Instance pure_beta f x (erec : expr) (v1 v2 : val) `{AsRecV v1 f x erec} :
+  PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
+Proof. unfold AsRecV in *. solve_pure_exec. Qed.
+
+Instance pure_unop op v v' :
+  PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
 Proof. solve_pure_exec. Qed.
 
-Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
-  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op e1 e2) (of_val v').
+Instance pure_binop op v1 v2 v' :
+  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v').
 Proof. solve_pure_exec. Qed.
 
-Instance pure_if_true e1 e2 : PureExec True 1 (If (Lit (LitBool true)) e1 e2) e1.
+Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
 Proof. solve_pure_exec. Qed.
 
-Instance pure_if_false e1 e2 : PureExec True 1 (If (Lit (LitBool false)) e1 e2) e2.
+Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
 Proof. solve_pure_exec. Qed.
 
-Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
-  PureExec True 1 (Fst (Pair e1 e2)) e1.
+Instance pure_fst v1 v2 :
+  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
 Proof. solve_pure_exec. Qed.
 
-Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
-  PureExec True 1 (Snd (Pair e1 e2)) e2.
+Instance pure_snd v1 v2 :
+  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
 Proof. solve_pure_exec. Qed.
 
-Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
-  PureExec True 1 (Case (InjL e0) e1 e2) (App e1 e0).
+Instance pure_case_inl v e1 e2 :
+  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
 Proof. solve_pure_exec. Qed.
 
-Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
-  PureExec True 1 (Case (InjR e0) e1 e2) (App e2 e0).
+Instance pure_case_inr v e1 e2 :
+  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
 Proof. solve_pure_exec. Qed.
 
 Section lifting.
@@ -131,21 +140,19 @@ Proof.
 Qed.
 
 (** Heap *)
-Lemma wp_alloc s E e v :
-  IntoVal e v →
-  {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
+Lemma wp_alloc s E v :
+  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
-  iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs) "[Hσ Hκs] !>"; iSplit; first by eauto.
+  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 κ κs) "[Hσ Hκs] !>"; iSplit; first by auto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
-Lemma twp_alloc s E e v :
-  IntoVal e v →
-  [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
+Lemma twp_alloc s E v :
+  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
 Proof.
-  iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit; first by eauto.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
@@ -153,7 +160,7 @@ Proof.
 Qed.
 
 Lemma wp_load s E l q v :
-  {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}.
+  {{{ ▷ l ↦{q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{q} v }}}.
 Proof.
   iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -161,7 +168,7 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_load s E l q v :
-  [[{ l ↦{q} v }]] Load (Lit (LitLoc l)) @ s; E [[{ RET v; l ↦{q} v }]].
+  [[{ l ↦{q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{q} v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -169,22 +176,22 @@ Proof.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_store s E l v' e v :
-  IntoVal e v →
-  {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l ↦ v }}}.
+Lemma wp_store s E l v' v :
+  {{{ ▷ l ↦ v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
+  {{{ RET LitV LitUnit; l ↦ v }}}.
 Proof.
-  iIntros (<- Φ) ">Hl HΦ".
+  iIntros (Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
-Lemma twp_store s E l v' e v :
-  IntoVal e v →
-  [[{ l ↦ v' }]] Store (Lit (LitLoc l)) e @ s; E [[{ RET LitV LitUnit; l ↦ v }]].
+Lemma twp_store s E l v' v :
+  [[{ l ↦ v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E
+  [[{ RET LitV LitUnit; l ↦ v }]].
 Proof.
-  iIntros (<- Φ) "Hl HΦ".
+  iIntros (Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
@@ -192,73 +199,65 @@ Proof.
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_fail s E l q v' e1 v1 e2 :
-  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 → vals_cas_compare_safe v' v1 →
-  {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
+Lemma wp_cas_fail s E l q v' v1 v2 :
+  v' ≠ v1 → vals_cas_compare_safe v' v1 →
+  {{{ ▷ l ↦{q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
 Proof.
-  iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
-Lemma twp_cas_fail s E l q v' e1 v1 e2 :
-  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 → vals_cas_compare_safe v' v1 →
-  [[{ l ↦{q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
+Lemma twp_cas_fail s E l q v' v1 v2 :
+  v' ≠ v1 → vals_cas_compare_safe v' v1 →
+  [[{ l ↦{q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   [[{ RET LitV (LitBool false); l ↦{q} v' }]].
 Proof.
-  iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
-  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_suc s E l e1 v1 e2 v2 :
-  IntoVal e1 v1 → IntoVal e2 v2 → vals_cas_compare_safe v1 v1 →
-  {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
+Lemma wp_cas_suc s E l v1 v2 :
+  vals_cas_compare_safe v1 v1 →
+  {{{ ▷ l ↦ v1 }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   {{{ RET LitV (LitBool true); l ↦ v2 }}}.
 Proof.
-  iIntros (<- <- ? Φ) ">Hl HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
-Lemma twp_cas_suc s E l e1 v1 e2 v2 :
-  IntoVal e1 v1 → IntoVal e2 v2 → vals_cas_compare_safe v1 v1 →
-  [[{ l ↦ v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
+Lemma twp_cas_suc s E l v1 v2 :
+  vals_cas_compare_safe v1 v1 →
+  [[{ l ↦ v1 }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   [[{ RET LitV (LitBool true); l ↦ v2 }]].
 Proof.
-  iIntros (<- <- ? Φ) "Hl HΦ".
-  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_faa s E l i1 e2 i2 :
-  IntoVal e2 (LitV (LitInt i2)) →
-  {{{ ▷ l ↦ LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ s; E
+Lemma wp_faa s E l i1 i2 :
+  {{{ ▷ l ↦ LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
   {{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }}}.
 Proof.
-  iIntros (<- Φ) ">Hl HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
-Lemma twp_faa s E l i1 e2 i2 :
-  IntoVal e2 (LitV (LitInt i2)) →
-  [[{ l ↦ LitV (LitInt i1) }]] FAA (Lit (LitLoc l)) e2 @ s; E
+Lemma twp_faa s E l i1 i2 :
+  [[{ l ↦ LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
   [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
 Proof.
-  iIntros (<- Φ) "Hl HΦ".
-  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
new file mode 100644
index 0000000000000000000000000000000000000000..d51fe924016560086a1127ed3d467bb097f36ab1
--- /dev/null
+++ b/theories/heap_lang/metatheory.v
@@ -0,0 +1,118 @@
+From iris.heap_lang Require Export lang.
+From stdpp Require Import gmap.
+
+(* This file contains some metatheory about the heap_lang language,
+  which is not needed for verifying programs. *)
+
+(* Closed expressions and values. *)
+Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
+  match e with
+  | Val v => is_closed_val v
+  | Var x => bool_decide (x ∈ X)
+  | Rec f x e => is_closed_expr (f :b: x :b: X) e
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
+     is_closed_expr X e
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2
+  | ResolveProph e1 e2 =>
+     is_closed_expr X e1 && is_closed_expr X e2
+  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
+     is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
+  | NewProph => true
+  end
+with is_closed_val (v : val) : bool :=
+  match v with
+  | LitV _ => true
+  | RecV f x e => is_closed_expr (f :b: x :b: []) e
+  | PairV v1 v2 => is_closed_val v1 && is_closed_val v2
+  | InjLV v | InjRV v => is_closed_val v
+  end.
+
+Lemma is_closed_weaken X Y e : is_closed_expr X e → X ⊆ Y → is_closed_expr Y e.
+Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
+
+Lemma is_closed_weaken_nil X e : is_closed_expr [] e → is_closed_expr X e.
+Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
+
+Lemma is_closed_subst X e x v :
+  is_closed_val v → is_closed_expr (x :: X) e → is_closed_expr X (subst x v e).
+Proof.
+  intros Hv. revert X.
+  induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
+    try match goal with
+    | H : ¬(_ ∧ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
+    end; eauto using is_closed_weaken with set_solver.
+Qed.
+Lemma is_closed_subst' X e x v :
+  is_closed_val v → is_closed_expr (x :b: X) e → is_closed_expr X (subst' x v e).
+Proof. destruct x; eauto using is_closed_subst. Qed.
+
+(* Substitution *)
+Lemma subst_is_closed X e x es : is_closed_expr X e → x ∉ X → subst x es e = e.
+Proof.
+  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
+    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
+Qed.
+
+Lemma subst_is_closed_nil e x v : is_closed_expr [] e → subst x v e = e.
+Proof. intros. apply subst_is_closed with []; set_solver. Qed.
+
+Lemma subst_subst e x v v' :
+  subst x v (subst x v' e) = subst x v' e.
+Proof.
+  intros. induction e; simpl; try (f_equal; by auto);
+    simplify_option_eq; auto using subst_is_closed_nil with f_equal.
+Qed.
+Lemma subst_subst' e x v v' :
+  subst' x v (subst' x v' e) = subst' x v' e.
+Proof. destruct x; simpl; auto using subst_subst. Qed.
+
+Lemma subst_subst_ne e x y v v' :
+  x ≠ y → subst x v (subst y v' e) = subst y v' (subst x v e).
+Proof.
+  intros. induction e; simpl; try (f_equal; by auto);
+    simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
+Qed.
+Lemma subst_subst_ne' e x y v v' :
+  x ≠ y → subst' x v (subst' y v' e) = subst' y v' (subst' x v e).
+Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.
+
+Lemma subst_rec' f y e x v :
+  x = f ∨ x = y ∨ x = BAnon →
+  subst' x v (Rec f y e) = Rec f y e.
+Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
+Lemma subst_rec_ne' f y e x v :
+  (x ≠ f ∨ f = BAnon) → (x ≠ y ∨ y = BAnon) →
+  subst' x v (Rec f y e) = Rec f y (subst' x v e).
+Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
+
+(* The stepping relation preserves closedness *)
+Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
+  is_closed_expr [] e1 →
+  (∀ x v, σ1.(heap) !! x = Some v → is_closed_val v) →
+  head_step e1 σ1 obs e2 σ2 es →
+
+  is_closed_expr [] e2 ∧ Forall (is_closed_expr []) es ∧
+  (∀ x v, σ2.(heap) !! x = Some v → is_closed_val v).
+Proof.
+  intros Cl1 Clσ1 STEP.
+  destruct STEP; simpl in *; split_and!; try by naive_solver.
+  - subst. repeat apply is_closed_subst'; naive_solver.
+  - unfold un_op_eval in *. repeat case_match; naive_solver.
+  - unfold bin_op_eval, bin_op_eval_bool in *. repeat case_match; naive_solver.
+  - intros ??.
+    match goal with
+    | |- context [<[?l1 := _]>_!! ?l2] => destruct (decide (l1 = l2)) as [->|]
+    end; rewrite ?lookup_insert ?lookup_insert_ne; naive_solver.
+  - intros ??.
+    match goal with
+    | |- context [<[?l1 := _]>_!! ?l2] => destruct (decide (l1 = l2)) as [->|]
+    end; rewrite ?lookup_insert ?lookup_insert_ne; naive_solver.
+  - intros ??.
+    match goal with
+    | |- context [<[?l1 := _]>_!! ?l2] => destruct (decide (l1 = l2)) as [->|]
+    end; rewrite ?lookup_insert ?lookup_insert_ne; naive_solver.
+  - intros ??.
+    match goal with
+    | |- context [<[?l1 := _]>_!! ?l2] => destruct (decide (l1 = l2)) as [->|]
+    end; rewrite ?lookup_insert ?lookup_insert_ne; naive_solver.
+Qed.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 01cec440238754c6f07e95142acf1e5485ec18a3..dc3fda17d6ce28e08f9c7f975e052103eb583700 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -11,7 +11,7 @@ Coercion LitLoc : loc >-> base_lit.
 Coercion LitProphecy : proph_id >-> base_lit.
 
 Coercion App : expr >-> Funclass.
-Coercion of_val : val >-> expr.
+Coercion Val : val >-> expr.
 
 Coercion Var : string >-> expr.
 
@@ -21,7 +21,6 @@ Notation "<>" := BAnon : binder_scope.
 (* No scope for the values, does not conflict and scope is often not inferred
 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.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
@@ -139,15 +138,14 @@ Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
 
 (* Shortcircuit Boolean connectives *)
 Notation "e1 && e2" :=
-  (If e1%E e2%E (Lit (LitBool false))) (only parsing) : expr_scope.
+  (If e1%E e2%E (LitV (LitBool false))) (only parsing) : expr_scope.
 Notation "e1 || e2" :=
-  (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
+  (If e1%E (LitV (LitBool true)) e2%E) (only parsing) : expr_scope.
 
 (** Notations for option *)
-Notation NONE := (InjL (Lit LitUnit)) (only parsing).
-Notation SOME x := (InjR x) (only parsing).
-
+Notation NONE := (InjL (LitV LitUnit)) (only parsing).
 Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
+Notation SOME x := (InjR x) (only parsing).
 Notation SOMEV x := (InjRV x) (only parsing).
 
 Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 979c7773d5ba82c088ce24c1edc730bea7592a6a..5b36ffb6230b84407fcc1339a502a0eb05c21735 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -28,7 +28,6 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
   end.
 
 Ltac wp_expr_simpl := wp_expr_eval simpl.
-Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
 
 Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
@@ -49,19 +48,15 @@ Proof.
   rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
 Qed.
 
-Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
-  IntoVal e v →
-  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E {{ Φ }}).
-Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
-Lemma tac_twp_value `{heapG Σ} Δ s E Φ e v :
-  IntoVal e v →
-  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E [{ Φ }]).
-Proof. rewrite envs_entails_eq=> ? ->. by apply twp_value. Qed.
+Lemma tac_wp_value `{heapG Σ} Δ s E Φ v :
+  envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
+Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
+Lemma tac_twp_value `{heapG Σ} Δ s E Φ v :
+  envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
+Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
 
 Ltac wp_value_head :=
-  first [eapply tac_wp_value || eapply tac_twp_value];
-    [iSolveTC
-    |reduction.pm_prettify; iEval (simpl of_val)].
+  first [eapply tac_wp_value || eapply tac_twp_value]; reduction.pm_prettify.
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
@@ -74,7 +69,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       [iSolveTC                       (* PureExec *)
       |try fast_done                  (* The pure condition for PureExec *)
       |iSolveTC                       (* IntoLaters *)
-      |wp_expr_simpl_subst; try wp_value_head (* new goal *)
+      |wp_expr_simpl; try wp_value_head (* new goal *)
       ])
     || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
@@ -84,34 +79,37 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       eapply (tac_twp_pure _ _ _ (fill K e'));
       [iSolveTC                       (* PureExec *)
       |try fast_done                  (* The pure condition for PureExec *)
-      |wp_expr_simpl_subst; try wp_value_head (* new goal *)
+      |wp_expr_simpl; try wp_value_head (* new goal *)
       ])
     || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
 Tactic Notation "wp_if" := wp_pure (If _ _ _).
-Tactic Notation "wp_if_true" := wp_pure (If (Lit (LitBool true)) _ _).
-Tactic Notation "wp_if_false" := wp_pure (If (Lit (LitBool false)) _ _).
+Tactic Notation "wp_if_true" := wp_pure (If (LitV (LitBool true)) _ _).
+Tactic Notation "wp_if_false" := wp_pure (If (LitV (LitBool false)) _ _).
 Tactic Notation "wp_unop" := wp_pure (UnOp _ _).
 Tactic Notation "wp_binop" := wp_pure (BinOp _ _ _).
 Tactic Notation "wp_op" := wp_unop || wp_binop.
 Tactic Notation "wp_rec" := wp_pure (App _ _).
 Tactic Notation "wp_lam" := wp_rec.
-Tactic Notation "wp_let" := wp_lam.
-Tactic Notation "wp_seq" := wp_lam.
+Tactic Notation "wp_let" := wp_pure (Rec BAnon (BNamed _) _); wp_lam.
+Tactic Notation "wp_seq" := wp_pure (Rec BAnon BAnon _); wp_lam.
 Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
 Tactic Notation "wp_case" := wp_pure (Case _ _ _).
-Tactic Notation "wp_match" := wp_case; wp_let.
+Tactic Notation "wp_match" := wp_case; wp_pure (Rec _ _ _); wp_lam.
+Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
+Tactic Notation "wp_pair" := wp_pure (Pair _ _).
+Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
 
 Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
-  envs_entails Δ (WP e @ s; E {{ v, WP f (of_val v) @ s; E {{ Φ }} }})%I →
+  envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
 Lemma tac_twp_bind `{heapG Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
-  envs_entails Δ (WP e @ s; E [{ v, WP f (of_val v) @ s; E [{ Φ }] }])%I →
+  envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I →
   envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_eq=> -> ->. by apply: twp_bind. Qed.
 
@@ -144,29 +142,29 @@ Context `{heapG Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (uPredI (iResUR Σ)).
+Implicit Types v : val.
+Implicit Types z : Z.
 
-Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
-  IntoVal e v →
+Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ s; E {{ Φ }})) →
-  envs_entails Δ (WP fill K (Alloc e) @ s; E {{ Φ }}).
+    envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (Alloc v) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ?? HΔ.
+  rewrite envs_entails_eq=> ? HΔ.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
 Qed.
-Lemma tac_twp_alloc Δ s E j K e v Φ :
-  IntoVal e v →
+Lemma tac_twp_alloc Δ s E j K v Φ :
   (∀ l, ∃ Δ',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ = Some Δ' ∧
-    envs_entails Δ' (WP fill K (Lit (LitLoc l)) @ s; E [{ Φ }])) →
-  envs_entails Δ (WP fill K (Alloc e) @ s; E [{ Φ }]).
+    envs_entails Δ' (WP fill K (Val $ LitV l) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (Alloc v) @ s; E [{ Φ }]).
 Proof.
-  rewrite envs_entails_eq=> ? HΔ.
+  rewrite envs_entails_eq=> HΔ.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
   rewrite left_id. apply forall_intro=> l.
   destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
@@ -176,8 +174,8 @@ Qed.
 Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  envs_entails Δ' (WP fill K (of_val v) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E {{ Φ }}).
+  envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ???.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
@@ -186,8 +184,8 @@ Proof.
 Qed.
 Lemma tac_twp_load Δ s E i K l q v Φ :
   envs_lookup i Δ = Some (false, l ↦{q} v)%I →
-  envs_entails Δ (WP fill K (of_val v) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E [{ Φ }]).
+  envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=> ??.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
@@ -195,25 +193,23 @@ Proof.
   by apply sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
-  IntoVal e v' →
+Lemma tac_wp_store Δ Δ' Δ'' s E i K l v v' Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  envs_entails Δ'' (WP fill K (Lit LitUnit) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Store (LitV l) (Val v')) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ?????.
+  rewrite envs_entails_eq=> ????.
   rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
-Lemma tac_twp_store Δ Δ' s E i K l v e v' Φ :
-  IntoVal e v' →
+Lemma tac_twp_store Δ Δ' s E i K l v v' Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ = Some Δ' →
-  envs_entails Δ' (WP fill K (Lit LitUnit) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E [{ Φ }]).
+  envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (Store (LitV l) v') @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq. intros. rewrite -twp_bind.
   eapply wand_apply; first by eapply twp_store.
@@ -221,121 +217,113 @@ Proof.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
-  IntoVal e1 v1 → IntoVal e2 v2 →
+Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   vals_cas_compare_safe v v1 →
-  (v = v1 → envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }})) →
-  (v ≠ v1 → envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }})) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
+  (v = v1 → envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})) →
+  (v ≠ v1 → envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ?????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
+  rewrite envs_entails_eq=> ???? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
   - rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
     rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
     apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
   - rewrite -wp_bind. eapply wand_apply.
-    { eapply wp_cas_fail; eauto. by eexists. }
+    { eapply wp_cas_fail; eauto. }
     rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
     apply later_mono, sep_mono_r. apply wand_mono; auto.
 Qed.
-Lemma tac_twp_cas Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
-  IntoVal e1 v1 → IntoVal e2 v2 →
+Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
   vals_cas_compare_safe v v1 →
-  (v = v1 → envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }])) →
-  (v ≠ v1 → envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }])) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
+  (v = v1 → envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }])) →
+  (v ≠ v1 → envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
-  rewrite envs_entails_eq=> ????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
+  rewrite envs_entails_eq=> ??? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
   - rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
     rewrite /= {1}envs_simple_replace_sound //; simpl.
     apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
   - rewrite -twp_bind. eapply wand_apply.
-    { eapply twp_cas_fail; eauto. by eexists. }
+    { eapply twp_cas_fail; eauto. }
     rewrite /= {1}envs_lookup_split //; simpl.
     apply sep_mono_r. apply wand_mono; auto.
 Qed.
 
-Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
-  IntoVal e1 v1 → AsVal e2 →
+Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   v ≠ v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
+  envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ???????.
+  rewrite envs_entails_eq=> ?????.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
-Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ :
-  IntoVal e1 v1 → AsVal e2 →
+Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦{q} v)%I →
   v ≠ v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
+  envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq. intros. rewrite -twp_bind.
   eapply wand_apply; first exact: twp_cas_fail.
   rewrite envs_lookup_split //=. by do 2 f_equiv.
 Qed.
 
-Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
-  IntoVal e1 v1 → IntoVal e2 v2 →
+Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   v = v1 → val_is_unboxed v →
-  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ????????; subst.
+  rewrite envs_entails_eq=> ??????; subst.
   rewrite -wp_bind. eapply wand_apply.
   { eapply wp_cas_suc; eauto. by left. }
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
-Lemma tac_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
-  IntoVal e1 v1 → IntoVal e2 v2 →
+Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
   v = v1 → val_is_unboxed v →
-  envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
+  envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
-  rewrite envs_entails_eq. intros; subst.
+  rewrite envs_entails_eq=>?????; subst.
   rewrite -twp_bind. eapply wand_apply.
   { eapply twp_cas_suc; eauto. by left. }
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
-  IntoVal e2 (LitV (LitInt i2)) →
+Lemma tac_wp_faa Δ Δ' Δ'' s E i K l z1 z2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦ LitV (LitInt i1))%I →
-  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (i1 + i2)))) Δ' = Some Δ'' →
-  envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E {{ Φ }}).
+  envs_lookup i Δ' = Some (false, l ↦ LitV z1)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (z1 + z2))) Δ' = Some Δ'' →
+  envs_entails Δ'' (WP fill K (Val $ LitV z1) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ?????; subst.
-  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ i1 _ i2).
+  rewrite envs_entails_eq=> ????.
+  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ z1 z2).
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
-Lemma tac_twp_faa Δ Δ' s E i K l i1 e2 i2 Φ :
-  IntoVal e2 (LitV (LitInt i2)) →
-  envs_lookup i Δ = Some (false, l ↦ LitV (LitInt i1))%I →
-  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (i1 + i2)))) Δ = Some Δ' →
-  envs_entails Δ' (WP fill K (Lit (LitInt i1)) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E [{ Φ }]).
+Lemma tac_twp_faa Δ Δ' s E i K l z1 z2 Φ :
+  envs_lookup i Δ = Some (false, l ↦ LitV z1)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (z1 + z2))) Δ = Some Δ' →
+  envs_entails Δ' (WP fill K (Val $ LitV z1) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E [{ Φ }]).
 Proof.
-  rewrite envs_entails_eq=> ????; subst.
-  rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ i1 _ i2).
+  rewrite envs_entails_eq=> ???.
+  rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ z1 z2).
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
@@ -370,15 +358,13 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_alloc _ _ _ _ Htmp K); [iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ Htmp K))
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     [iSolveTC
     |finish ()]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_alloc _ _ _ Htmp K); [iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K))
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     finish ()
   | _ => fail "wp_alloc: not a 'wp'"
@@ -414,13 +400,12 @@ Tactic Notation "wp_store" :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
     iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
   let finish _ :=
-    wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head] in
+    wp_expr_simpl; try first [wp_seq|wp_value_head] in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_store _ _ _ _ _ _ K); [iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ _ K))
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [iSolveTC
     |solve_mapsto ()
@@ -428,8 +413,7 @@ Tactic Notation "wp_store" :=
     |finish ()]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_store _ _ _ _ _ K); [iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_store _ _ _ _ _ K))
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [solve_mapsto ()
     |pm_reflexivity
@@ -445,8 +429,7 @@ Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_cas _ _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas _ _ _ _ _ _ K))
       |fail 1 "wp_cas: cannot find 'CAS' in" e];
     [iSolveTC
     |solve_mapsto ()
@@ -456,8 +439,7 @@ Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2
     |intros H2; wp_expr_simpl; try wp_value_head]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_cas _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas _ _ _ _ _ K))
       |fail 1 "wp_cas: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |pm_reflexivity
@@ -475,8 +457,7 @@ Tactic Notation "wp_cas_fail" :=
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_cas_fail _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ _ K))
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [iSolveTC
     |solve_mapsto ()
@@ -485,8 +466,7 @@ Tactic Notation "wp_cas_fail" :=
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_cas_fail _ _ _ _ K); [iSolveTC|iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
@@ -503,8 +483,7 @@ Tactic Notation "wp_cas_suc" :=
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ _ K))
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [iSolveTC
     |solve_mapsto ()
@@ -514,8 +493,7 @@ Tactic Notation "wp_cas_suc" :=
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_cas_suc _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |pm_reflexivity
@@ -533,8 +511,7 @@ Tactic Notation "wp_faa" :=
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_faa _ _ _ _ _ _ K); [iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ _ K))
       |fail 1 "wp_faa: cannot find 'CAS' in" e];
     [iSolveTC
     |solve_mapsto ()
@@ -542,8 +519,7 @@ Tactic Notation "wp_faa" :=
     |wp_expr_simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_faa _ _ _ _ _ K); [iSolveTC|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_faa _ _ _ _ _ K))
       |fail 1 "wp_faa: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |pm_reflexivity
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index d0cca5401f823ae2782e46e5d2e42adf42eb9fbb..cb1a3f78deda8a4b143806a2633a79a43f9062c5 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -2,293 +2,90 @@ From iris.heap_lang Require Export lang.
 Set Default Proof Using "Type".
 Import heap_lang.
 
-(** We define an alternative representation of expressions in which the
-embedding of values and closed expressions is explicit. By reification of
-expressions into this type we can implementation substitution, closedness
-checking, atomic checking, and conversion into values, by computation. *)
-Module W.
-Inductive expr :=
-  (* Value together with the original expression *)
-  | Val (v : val) (e : heap_lang.expr) (H : to_val e = Some v)
-  | ClosedExpr (e : heap_lang.expr) `{!Closed [] e}
-  (* Base lambda calculus *)
-  | 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)
-  | BinOp (op : bin_op) (e1 e2 : expr)
-  | If (e0 e1 e2 : expr)
-  (* Products *)
-  | Pair (e1 e2 : expr)
-  | Fst (e : expr)
-  | Snd (e : expr)
-  (* Sums *)
-  | InjL (e : expr)
-  | InjR (e : expr)
-  | Case (e0 : expr) (e1 : expr) (e2 : expr)
-  (* Concurrency *)
-  | Fork (e : expr)
-  (* Heap *)
-  | Alloc (e : expr)
-  | Load (e : expr)
-  | Store (e1 : expr) (e2 : expr)
-  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
-  | FAA (e1 : expr) (e2 : expr)
-  | NewProph
-  | ResolveProph (e1 : expr) (e2 : expr).
+Instance into_val_val v : IntoVal (Val v) v.
+Proof. done. Qed.
+Instance as_val_val v : AsVal (Val v).
+Proof. by eexists. Qed.
 
-Fixpoint to_expr (e : expr) : heap_lang.expr :=
-  match e with
-  | Val v e' _ => e'
-  | ClosedExpr e => e
-  | Var x => heap_lang.Var x
-  | Rec f x e => heap_lang.Rec f x (to_expr e)
-  | App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
-  | Lit l => heap_lang.Lit l
-  | UnOp op e => heap_lang.UnOp op (to_expr e)
-  | BinOp op e1 e2 => heap_lang.BinOp op (to_expr e1) (to_expr e2)
-  | If e0 e1 e2 => heap_lang.If (to_expr e0) (to_expr e1) (to_expr e2)
-  | Pair e1 e2 => heap_lang.Pair (to_expr e1) (to_expr e2)
-  | Fst e => heap_lang.Fst (to_expr e)
-  | Snd e => heap_lang.Snd (to_expr e)
-  | InjL e => heap_lang.InjL (to_expr e)
-  | InjR e => heap_lang.InjR (to_expr e)
-  | Case e0 e1 e2 => heap_lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
-  | Fork e => heap_lang.Fork (to_expr e)
-  | Alloc e => heap_lang.Alloc (to_expr e)
-  | Load e => heap_lang.Load (to_expr e)
-  | Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
-  | CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
-  | FAA e1 e2 => heap_lang.FAA (to_expr e1) (to_expr e2)
-  | NewProph => heap_lang.NewProph
-  | ResolveProph e1 e2 => heap_lang.ResolveProph (to_expr e1) (to_expr e2)
-  end.
-
-Ltac of_expr e :=
-  lazymatch e with
-  | heap_lang.Var ?x => constr:(Var x)
-  | heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
-  | heap_lang.App ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
-  | heap_lang.Lit ?l => constr:(Lit l)
-  | heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
-  | heap_lang.BinOp ?op ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
-  | heap_lang.If ?e0 ?e1 ?e2 =>
-     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
-     constr:(If e0 e1 e2)
-  | heap_lang.Pair ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
-  | heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
-  | heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
-  | heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
-  | heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
-  | heap_lang.Case ?e0 ?e1 ?e2 =>
-     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
-     constr:(Case e0 e1 e2)
-  | heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
-  | heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
-  | heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
-  | heap_lang.Store ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
-  | heap_lang.CAS ?e0 ?e1 ?e2 =>
-     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
-     constr:(CAS e0 e1 e2)
-  | heap_lang.FAA ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
-  | heap_lang.NewProph =>
-     constr:(NewProph)
-  | heap_lang.ResolveProph ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(ResolveProph e1 e2)
-  | to_expr ?e => e
-  | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
-  | language.of_val ?v => constr:(Val v (of_val v) (to_of_val v))
-  | _ => match goal with
-         | H : to_val e = Some ?v |- _ => constr:(Val v e H)
-         | H : Closed [] e |- _ => constr:(@ClosedExpr e H)
-         end
-  end.
-
-Fixpoint is_closed (X : list string) (e : expr) : bool :=
-  match e with
-  | Val _ _ _ | ClosedExpr _ => true
-  | Var x => bool_decide (x ∈ X)
-  | Rec f x e => is_closed (f :b: x :b: X) e
-  | Lit _ | NewProph => 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 | FAA e1 e2 | ResolveProph 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.
-Lemma is_closed_correct X e : is_closed X e → heap_lang.is_closed X (to_expr e).
+Instance alloc_atomic s v : Atomic s (Alloc (Val v)).
 Proof.
-  revert X.
-  induction e; naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - intros σ e σ' ef obs Hstep; simpl in *. inversion Hstep; simplify_eq. eauto.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
+    destruct Ki; simplify_eq/=. eauto.
 Qed.
-
-(* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
-constructors are only generated for closed expressions of which we know nothing
-about apart from being closed. Notice that the reverse implication of
-[to_val_Some] thus does not hold. *)
-Fixpoint to_val (e : expr) : option val :=
-  match e with
-  | Val v _ _ => Some v
-  | Rec f x e =>
-     if decide (is_closed (f :b: x :b: []) e) is left H
-     then Some (@RecV f x (to_expr e) (is_closed_correct _ _ H)) 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
-  | InjR e => InjRV <$> to_val e
-  | _ => None
-  end.
-Lemma to_val_Some e v :
-  to_val e = Some v → heap_lang.of_val v = W.to_expr e.
+Instance load_atomic s v : Atomic s (Load (Val v)).
 Proof.
-  revert v. induction e; intros; simplify_option_eq; try f_equal; auto using of_to_val.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - intros σ e σ' ef obs Hstep; simpl in *. inversion Hstep; simplify_eq. eauto.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
+    destruct Ki; simplify_eq/=. eauto.
 Qed.
-Lemma to_val_is_Some e :
-  is_Some (to_val e) → ∃ v, heap_lang.of_val v = to_expr e.
-Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
-
-Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
-  match e with
-  | Val v e H => Val v e H
-  | ClosedExpr e => ClosedExpr e
-  | Var y => if decide (x = y) then es else Var y
-  | Rec f y e =>
-     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 (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)
-  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
-  | NewProph => NewProph
-  | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
-  end.
-Lemma to_expr_subst x er e :
-  to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
+Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
 Proof.
-  induction e; simpl; repeat case_decide;
-    f_equal; eauto using subst_is_closed_nil, is_closed_to_val, eq_sym.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - intros σ e σ' ef obs Hstep; simpl in *. inversion Hstep; simplify_eq. eauto.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
+    destruct Ki; simplify_eq/=; eauto.
 Qed.
-
-Definition is_atomic (e : expr) :=
-  match e with
-  | Alloc e => bool_decide (is_Some (to_val e))
-  | Load e => bool_decide (is_Some (to_val e))
-  | Store e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
-  | CAS e0 e1 e2 =>
-     bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
-  | FAA e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
-  | Fork _ => true
-  (* Make "skip" atomic *)
-  | App (Rec _ _ (Lit _)) (Lit _) => true
-  | NewProph => true
-  | ResolveProph e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
-  | _ => false
-  end.
-Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
+Instance cas_atomic s v0 v1 v2 : Atomic s (CAS (Val v0) (Val v1) (Val v2)).
 Proof.
-  intros He. apply strongly_atomic_atomic, ectx_language_atomic.
-  - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
-    destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
-      inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
-    unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - intros σ e σ' ef obs Hstep; simpl in *. inversion Hstep; simplify_eq; eauto.
   - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
-    destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//); try
-      naive_solver eauto using as_val_is_Some, to_val_is_Some.
+    destruct Ki; simplify_eq/=; eauto.
+Qed.
+Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
+Proof.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - intros σ e σ' ef obs Hstep; simpl in *. inversion Hstep; simplify_eq; eauto.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
+    destruct Ki; simplify_eq/=; eauto.
+Qed.
+Instance fork_atomic s e : Atomic s (Fork e).
+Proof.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - intros σ e' σ' ef obs Hstep; simpl in *. inversion Hstep; simplify_eq; eauto.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
+    destruct Ki; simplify_eq/=; eauto.
+Qed.
+Instance skip_atomic s : Atomic s Skip.
+Proof.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - intros σ e' σ' ef obs Hstep; simpl in *. inversion Hstep; simplify_eq; eauto.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
+    destruct Ki; simplify_eq/=; eauto.
+Qed.
+Instance new_proph_atomic s : Atomic s NewProph.
+Proof.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - intros σ e' σ' ef obs Hstep; simpl in *. inversion Hstep; simplify_eq; eauto.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
+    destruct Ki; simplify_eq/=; eauto.
+Qed.
+Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
+Proof.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - intros σ e σ' ef obs Hstep; simpl in *. inversion Hstep; simplify_eq. eauto.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
+    destruct Ki; simplify_eq/=; eauto.
 Qed.
-End W.
-
-Ltac solve_closed :=
-  match goal with
-  | |- Closed ?X ?e =>
-     let e' := W.of_expr e in change (Closed X (W.to_expr e'));
-     apply W.is_closed_correct; vm_compute; exact I
-  end.
-Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
-
-Ltac solve_into_val :=
-  match goal with
-  | |- IntoVal ?e ?v =>
-     let e' := W.of_expr e in change (of_val v = W.to_expr e');
-     apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
-  end.
-Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
-
-Ltac solve_as_val :=
-  match goal with
-  | |- AsVal ?e =>
-     let e' := W.of_expr e in change (∃ v, of_val v = W.to_expr e');
-     apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
-  end.
-Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
-
-Ltac solve_atomic :=
-  match goal with
-  | |- Atomic ?s ?e =>
-     let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
-     apply W.is_atomic_correct; vm_compute; exact I
-  end.
-Hint Extern 10 (Atomic _ _) => solve_atomic : typeclass_instances.
 
-(** Substitution *)
-Ltac simpl_subst :=
-  simpl;
-  repeat match goal with
-  | |- context [subst ?x ?er ?e] =>
-      let er' := W.of_expr er in let e' := W.of_expr e in
-      change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
-      rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
-  end;
-  unfold W.to_expr.
-Arguments W.to_expr : simpl never.
-Arguments subst : simpl never.
 
 (** The tactic [reshape_expr e tac] decomposes the expression [e] into an
 evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
 for each possible decomposition until [tac] succeeds. *)
-Ltac reshape_val e tac :=
-  let rec go e :=
-  lazymatch e with
-  | of_val ?v => v
-  | Rec ?f ?x ?e => constr:(RecV f x e)
-  | Lit ?l => constr:(LitV l)
-  | Pair ?e1 ?e2 =>
-    let v1 := go e1 in let v2 := go e2 in constr:(PairV v1 v2)
-  | InjL ?e => let v := go e in constr:(InjLV v)
-  | InjR ?e => let v := go e in constr:(InjRV v)
-  end in let v := go e in tac v.
-
 Ltac reshape_expr e tac :=
   let rec go K e :=
   match e with
   | _ => tac K e
-  | App ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (AppLCtx v2 :: K) e1)
+  | App ?e (Val ?v) => go (AppLCtx v :: K) e
   | App ?e1 ?e2 => go (AppRCtx e1 :: K) e2
   | UnOp ?op ?e => go (UnOpCtx op :: K) e
-  | BinOp ?op ?e1 ?e2 =>
-     reshape_val e2 ltac:(fun v2 => go (BinOpLCtx op v2 :: K) e1)
+  | BinOp ?op ?e (Val ?v) => go (BinOpLCtx op v :: K) e
   | BinOp ?op ?e1 ?e2 => go (BinOpRCtx op e1 :: K) e2
   | If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
-  | Pair ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (PairLCtx v2 :: K) e1)
+  | Pair ?e (Val ?v) => go (PairLCtx v :: K) e
   | Pair ?e1 ?e2 => go (PairRCtx e1 :: K) e2
   | Fst ?e => go (FstCtx :: K) e
   | Snd ?e => go (SndCtx :: K) e
@@ -297,14 +94,13 @@ Ltac reshape_expr e tac :=
   | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
   | Alloc ?e => go (AllocCtx :: K) e
   | Load ?e => go (LoadCtx :: K) e
-  | Store ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (StoreLCtx v2 :: K) e1)
+  | Store ?e (Val ?v) => go (StoreLCtx v :: K) e
   | Store ?e1 ?e2 => go (StoreRCtx e1 :: K) e2
-  | CAS ?e0 ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => first
-     [ reshape_val e1 ltac:(fun v1 => go (CasLCtx v1 v2 :: K) e0)
-     | go (CasMCtx e0 v2 :: K) e1 ])
+  | CAS ?e0 (Val ?v1) (Val ?v2) => go (CasLCtx v1 v2 :: K) e0
+  | CAS ?e0 ?e1 (Val ?v2) => go (CasMCtx e0 v2 :: K) e1
   | CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
-  | FAA ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (FaaLCtx v2 :: K) e1)
+  | FAA ?e (Val ?v) => go (FaaLCtx v :: K) e
   | FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
-  | ResolveProph ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (ProphLCtx v2 :: K) e1)
+  | ResolveProph ?e (Val ?v) => go (ProphLCtx v :: K) e
   | ResolveProph ?e1 ?e2 => go (ProphRCtx e1 :: K) e2
   end in go (@nil ectx_item) e.