From 9646293efd396bec09b87675637a0b30c0c23996 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 13 Sep 2018 00:01:30 +0200
Subject: [PATCH] A specific constructor for injecting values in expressions

We add a specific constructor to the type of expressions for injecting
values in expressions.

The advantage are :
- Values can be assumed to be always closed when performing
  substitutions (even though they could contain free variables, but it
  turns out it does not cause any problem in the proofs in
  practice). This means that we no longer need the `Closed` typeclass
  and everything that comes with it (all the reflection-based machinery
  contained in tactics.v is no longer necessary). I have not measured
  anything, but I guess this would have a significant performance
  impact.

- There is only one constructor for values. As a result, the AsVal and
  IntoVal typeclasses are no longer necessary: an expression which is
  a value will always unify with `Val _`, and therefore lemmas can be
  stated using this constructor.

Of course, this means that there are two ways of writing such a thing
as "The pair of integers 1 and 2": Either by using the value
constructor applied to the pair represented as a value, or by using
the expression pair constructor. So we add reduction rules that
transform reduced pair, injection and closure expressions into values.
At first, this seems weird, because of the redundancy. But in fact,
this has some meaning, since the machine migth actually be doing
something to e.g., allocate the pair or the closure.

These additional steps of computation show up in the proofs, and some
additional wp_* tactics need to be called.
---
 _CoqProject                          |   1 +
 tests/heap_lang.ref                  |  14 +-
 tests/heap_lang.v                    |   4 +
 tests/ipm_paper.v                    |   8 +-
 tests/list_reverse.ref               |   4 +-
 tests/list_reverse.v                 |   4 +-
 tests/one_shot.ref                   |   2 +-
 tests/one_shot.v                     |  10 +-
 tests/tree_sum.v                     |   2 +-
 theories/heap_lang/lang.v            | 484 ++++++++++++---------------
 theories/heap_lang/lib/assert.v      |   8 +-
 theories/heap_lang/lib/atomic_heap.v |  38 +--
 theories/heap_lang/lib/coin_flip.v   |   5 +-
 theories/heap_lang/lib/counter.v     |  10 +-
 theories/heap_lang/lib/increment.v   |   9 +-
 theories/heap_lang/lib/par.v         |  30 +-
 theories/heap_lang/lib/spawn.v       |   4 +-
 theories/heap_lang/lib/spin_lock.v   |   2 +-
 theories/heap_lang/lib/ticket_lock.v |   8 +-
 theories/heap_lang/lifting.v         | 151 +++++----
 theories/heap_lang/metatheory.v      | 118 +++++++
 theories/heap_lang/notation.v        |  12 +-
 theories/heap_lang/proofmode.v       | 212 ++++++------
 theories/heap_lang/tactics.v         | 336 ++++---------------
 24 files changed, 667 insertions(+), 809 deletions(-)
 create mode 100644 theories/heap_lang/metatheory.v

diff --git a/_CoqProject b/_CoqProject
index e587aa9aa..497e83782 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 b4ac2c10a..4d17b008c 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 922c56acd..976695e55 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 179183d14..ad39c2b1b 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 baa273268..2c8d90077 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 89b5963bb..39d00a142 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 a64d6fb6c..08d4ddb27 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 79faa4fd3..e39d64886 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 2e91d3417..b8760ad64 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 697a59f78..ad5d655d4 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 ce10822a0..4a7733f14 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 22adb5813..c88ba0204 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 65d05ea26..5647d1c2d 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 788eb8580..6ab8cbe5b 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 d26b43292..c6a3a92f2 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 eaf7d05cb..4691dfefc 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 acd4f0a8c..900f75786 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 f3cf0e072..5b010185c 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 caf6ff093..2da04f578 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 b7805d078..fe203669c 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 000000000..d51fe9240
--- /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 01cec4402..dc3fda17d 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 979c7773d..5b36ffb62 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 d0cca5401..cb1a3f78d 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.
-- 
GitLab