diff --git a/_CoqProject b/_CoqProject
index e51a099d67cbc1ffd0e30c384758a60bc0526cc6..b6f7406c4d9a347281b6c3f6f37afeea663f606c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -64,6 +64,7 @@ iris/language.v
 iris/functor.v
 iris/tests.v
 barrier/heap_lang.v
+barrier/heap_lang_tactics.v
 barrier/lifting.v
 barrier/sugar.v
 barrier/tests.v
diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index f58ee88c04e71f01a659eeac16fe068d853c564b..d2f508384deaf3f35f4cf13b0f83fd66a81acf15 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -1,447 +1,301 @@
 Require Export Autosubst.Autosubst.
-Require Import prelude.option prelude.gmap iris.language.
+Require Export iris.language.
+Require Import prelude.gmap.
 
-(** Expressions and values. *)
+Module heap_lang.
+(** Expressions and vals. *)
 Definition loc := positive. (* Really, any countable type. *)
 
 Inductive expr :=
-(* Base lambda calculus *)
-| Var (x : var)
-| Rec (e : {bind 2 of expr}) (* These are recursive lambdas. The *inner* binder is the recursive call! *)
-| App (e1 e2 : expr)
-(* Natural numbers *)
-| LitNat (n : nat)
-| Plus (e1 e2 : expr)
-| Le (e1 e2 : expr)
-(* Unit *)
-| LitUnit
-(* Products *)
-| Pair (e1 e2 : expr)
-| Fst (e : expr)
-| Snd (e : expr)
-(* Sums *)
-| InjL (e : expr)
-| InjR (e : expr)
-| Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
-(* Concurrency *)
-| Fork (e : expr)
-(* Heap *)
-| Loc (l : loc)
-| Alloc (e : expr)
-| Load (e : expr)
-| Store (e1 : expr) (e2 : expr)
-| Cas (e0 : expr) (e1 : expr) (e2 : expr)
-.
+  (* Base lambda calculus *)
+  | Var (x : var)
+  | Rec (e : {bind 2 of expr}) (* These are recursive lambdas.
+                                  The *inner* binder is the recursive call! *)
+  | App (e1 e2 : expr)
+  (* Natural numbers *)
+  | LitNat (n : nat)
+  | Plus (e1 e2 : expr)
+  | Le (e1 e2 : expr)
+  (* Unit *)
+  | LitUnit
+  (* Products *)
+  | Pair (e1 e2 : expr)
+  | Fst (e : expr)
+  | Snd (e : expr)
+  (* Sums *)
+  | InjL (e : expr)
+  | InjR (e : expr)
+  | Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
+  (* Concurrency *)
+  | Fork (e : expr)
+  (* Heap *)
+  | Loc (l : loc)
+  | Alloc (e : expr)
+  | Load (e : expr)
+  | Store (e1 : expr) (e2 : expr)
+  | Cas (e0 : expr) (e1 : expr) (e2 : expr).
 
 Instance Ids_expr : Ids expr. derive. Defined.
 Instance Rename_expr : Rename expr. derive. Defined.
 Instance Subst_expr : Subst expr. derive. Defined.
 Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
 
-(* This sugar is used by primitive reduction riles (<=, CAS) and hence defined here. *)
-Definition LitTrue := InjL LitUnit.
-Definition LitFalse := InjR LitUnit.
-
-Inductive value :=
-| RecV (e : {bind 2 of expr})
-| LitNatV (n : nat) (* These are recursive lambdas. The *inner* binder is the recursive call! *)
-| LitUnitV
-| PairV (v1 v2 : value)
-| InjLV (v : value)
-| InjRV (v : value)
-| LocV (l : loc)
-.
+(* This sugar is used by primitive reduction riles (<=, CAS) and hence
+defined here. *)
+Notation LitTrue := (InjL LitUnit).
+Notation LitFalse := (InjR LitUnit).
+
+Inductive val :=
+  | RecV (e : {bind 2 of expr}) (* These are recursive lambdas.
+                                   The *inner* binder is the recursive call! *)
+  | LitNatV (n : nat)
+  | LitUnitV
+  | PairV (v1 v2 : val)
+  | InjLV (v : val)
+  | InjRV (v : val)
+  | LocV (l : loc).
 
 Definition LitTrueV := InjLV LitUnitV.
 Definition LitFalseV := InjRV LitUnitV.
 
-Fixpoint v2e (v : value) : expr :=
+Fixpoint of_val (v : val) : expr :=
   match v with
-  | RecV e   => Rec e
+  | RecV e => Rec e
   | LitNatV n => LitNat n
   | LitUnitV => LitUnit
-  | PairV v1 v2 => Pair (v2e v1) (v2e v2)
-  | InjLV v => InjL (v2e v)
-  | InjRV v => InjR (v2e v)
+  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
+  | InjLV v => InjL (of_val v)
+  | InjRV v => InjR (of_val v)
   | LocV l => Loc l
   end.
-
-Fixpoint e2v (e : expr) : option value :=
+Fixpoint to_val (e : expr) : option val :=
   match e with
   | Rec e => Some (RecV e)
   | LitNat n => Some (LitNatV n)
   | LitUnit => Some LitUnitV
-  | Pair e1 e2 => v1 ← e2v e1;
-                  v2 ← e2v e2;
-                  Some (PairV v1 v2)
-  | InjL e => InjLV <$> e2v e
-  | InjR e => InjRV <$> e2v e
+  | 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
   | Loc l => Some (LocV l)
   | _ => None
   end.
 
-Lemma v2v v:
-  e2v (v2e v) = Some v.
-Proof.
-  induction v; simpl; rewrite ?IHv ?IHv1 /= ?IHv2; reflexivity.
-Qed.
-
-Section e2e. (* To get local tactics. *)
-Lemma e2e e v:
-  e2v e = Some v → v2e v = e.
-Proof.
-  Ltac case0 := case =><-; simpl; eauto using f_equal, f_equal2.
-  Ltac case1 e1 := destruct (e2v e1); simpl; [|discriminate];
-                   case0.
-  Ltac case2 e1 e2 := destruct (e2v e1); simpl; [|discriminate];
-                      destruct (e2v e2); simpl; [|discriminate];
-                      case0.
-
-  revert v; induction e; intros v; simpl; try discriminate;
-    by (case2 e1 e2 || case1 e || case0).
-Qed.
-End e2e.
-
-Lemma v2e_inj v1 v2:
-  v2e v1 = v2e v2 → v1 = v2.
-Proof.
-  revert v2; induction v1=>v2; destruct v2; simpl; try done;
-    case; eauto using f_equal, f_equal2.
-Qed.
-
-(** The state: heaps of values. *)
-Definition state := gmap loc value.
+(** The state: heaps of vals. *)
+Definition state := gmap loc val.
 
 (** Evaluation contexts *)
-Inductive ectx :=
-| EmptyCtx
-| AppLCtx (K1 : ectx)  (e2 : expr)
-| AppRCtx (v1 : value) (K2 : ectx)
-| PlusLCtx (K1 : ectx)  (e2 : expr)
-| PlusRCtx (v1 : value) (K2 : ectx)
-| LeLCtx (K1 : ectx)  (e2 : expr)
-| LeRCtx (v1 : value) (K2 : ectx)
-| PairLCtx (K1 : ectx)  (e2 : expr)
-| PairRCtx (v1 : value) (K2 : ectx)
-| FstCtx (K : ectx)
-| SndCtx (K : ectx)
-| InjLCtx (K : ectx)
-| InjRCtx (K : ectx)
-| CaseCtx (K : ectx) (e1 : {bind expr}) (e2 : {bind expr})
-| AllocCtx (K : ectx)
-| LoadCtx (K : ectx)
-| StoreLCtx (K1 : ectx)  (e2 : expr)
-| StoreRCtx (v1 : value) (K2 : ectx)
-| CasLCtx (K0 : ectx)  (e1 : expr)  (e2 : expr)
-| CasMCtx (v0 : value) (K1 : ectx)  (e2 : expr)
-| CasRCtx (v0 : value) (v1 : value) (K2 : ectx)
-.
-
-Fixpoint fill (K : ectx) (e : expr) :=
-  match K with
-  | EmptyCtx => e
-  | AppLCtx K1 e2 => App (fill K1 e) e2
-  | AppRCtx v1 K2 => App (v2e v1) (fill K2 e)
-  | PlusLCtx K1 e2 => Plus (fill K1 e) e2
-  | PlusRCtx v1 K2 => Plus (v2e v1) (fill K2 e)
-  | LeLCtx K1 e2 => Le (fill K1 e) e2
-  | LeRCtx v1 K2 => Le (v2e v1) (fill K2 e)
-  | PairLCtx K1 e2 => Pair (fill K1 e) e2
-  | PairRCtx v1 K2 => Pair (v2e v1) (fill K2 e)
-  | FstCtx K => Fst (fill K e)
-  | SndCtx K => Snd (fill K e)
-  | InjLCtx K => InjL (fill K e)
-  | InjRCtx K => InjR (fill K e)
-  | CaseCtx K e1 e2 => Case (fill K e) e1 e2
-  | AllocCtx K => Alloc (fill K e)
-  | LoadCtx K => Load (fill K e)
-  | StoreLCtx K1 e2 => Store (fill K1 e) e2
-  | StoreRCtx v1 K2 => Store (v2e v1) (fill K2 e)
-  | CasLCtx K0 e1 e2 => Cas (fill K0 e) e1 e2
-  | CasMCtx v0 K1 e2 => Cas (v2e v0) (fill K1 e) e2
-  | CasRCtx v0 v1 K2 => Cas (v2e v0) (v2e v1) (fill K2 e)
-  end.
-
-Fixpoint comp_ctx (Ko : ectx) (Ki : ectx) :=
-  match Ko with
-  | EmptyCtx => Ki
-  | AppLCtx K1 e2 => AppLCtx (comp_ctx K1 Ki) e2
-  | AppRCtx v1 K2 => AppRCtx v1 (comp_ctx K2 Ki)
-  | PlusLCtx K1 e2 => PlusLCtx (comp_ctx K1 Ki) e2
-  | PlusRCtx v1 K2 => PlusRCtx v1 (comp_ctx K2 Ki)
-  | LeLCtx K1 e2 => LeLCtx (comp_ctx K1 Ki) e2
-  | LeRCtx v1 K2 => LeRCtx v1 (comp_ctx K2 Ki)
-  | PairLCtx K1 e2 => PairLCtx (comp_ctx K1 Ki) e2
-  | PairRCtx v1 K2 => PairRCtx v1 (comp_ctx K2 Ki)
-  | FstCtx K => FstCtx (comp_ctx K Ki)
-  | SndCtx K => SndCtx (comp_ctx K Ki)
-  | InjLCtx K => InjLCtx (comp_ctx K Ki)
-  | InjRCtx K => InjRCtx (comp_ctx K Ki)
-  | CaseCtx K e1 e2 => CaseCtx (comp_ctx K Ki) e1 e2
-  | AllocCtx K => AllocCtx (comp_ctx K Ki)
-  | LoadCtx K => LoadCtx (comp_ctx K Ki)
-  | StoreLCtx K1 e2 => StoreLCtx (comp_ctx K1 Ki) e2
-  | StoreRCtx v1 K2 => StoreRCtx v1 (comp_ctx K2 Ki)
-  | CasLCtx K0 e1 e2 => CasLCtx (comp_ctx K0 Ki) e1 e2
-  | CasMCtx v0 K1 e2 => CasMCtx v0 (comp_ctx K1 Ki) e2
-  | CasRCtx v0 v1 K2 => CasRCtx v0 v1 (comp_ctx K2 Ki)
+Inductive ectx_item :=
+  | AppLCtx (e2 : expr)
+  | AppRCtx (v1 : val)
+  | PlusLCtx (e2 : expr)
+  | PlusRCtx (v1 : val)
+  | LeLCtx (e2 : expr)
+  | LeRCtx (v1 : val)
+  | PairLCtx (e2 : expr)
+  | PairRCtx (v1 : val)
+  | FstCtx
+  | SndCtx
+  | InjLCtx
+  | InjRCtx
+  | CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
+  | AllocCtx
+  | LoadCtx
+  | StoreLCtx (e2 : expr)
+  | StoreRCtx (v1 : val)
+  | CasLCtx (e1 : expr)  (e2 : expr)
+  | CasMCtx (v0 : val) (e2 : expr)
+  | CasRCtx (v0 : val) (v1 : val).
+Notation ectx := (list ectx_item).
+Implicit Types Ki : ectx_item.
+Implicit Types K : ectx.
+
+Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr :=
+  match Ki with
+  | AppLCtx e2 => App e e2
+  | AppRCtx v1 => App (of_val v1) e
+  | PlusLCtx e2 => Plus e e2
+  | PlusRCtx v1 => Plus (of_val v1) e
+  | LeLCtx e2 => Le e e2
+  | LeRCtx v1 => Le (of_val v1) e
+  | PairLCtx e2 => Pair e e2
+  | PairRCtx v1 => Pair (of_val v1) e
+  | FstCtx => Fst e
+  | SndCtx => Snd e
+  | InjLCtx => InjL e
+  | InjRCtx => InjR e
+  | CaseCtx e1 e2 => Case e e1 e2
+  | AllocCtx => Alloc e
+  | LoadCtx => Load e
+  | StoreLCtx e2 => Store e e2
+  | StoreRCtx v1 => Store (of_val v1) e
+  | CasLCtx e1 e2 => Cas e e1 e2
+  | CasMCtx v0 e2 => Cas (of_val v0) e e2
+  | CasRCtx v0 v1 => Cas (of_val v0) (of_val v1) e
   end.
+Instance ectx_fill : Fill ectx expr :=
+  fix go K e := let _ : Fill _ _ := @go in
+  match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) end.
 
-Lemma fill_empty e :
-  fill EmptyCtx e = e.
-Proof.
-  reflexivity.
-Qed.
-
-Lemma fill_comp K1 K2 e :
-  fill K1 (fill K2 e) = fill (comp_ctx K1 K2) e.
-Proof.
-  revert K2 e; induction K1 => K2 e /=; rewrite ?IHK1 ?IHK2; reflexivity.
-Qed.
-
-Lemma fill_inj_r K e1 e2 :
-  fill K e1 = fill K e2 → e1 = e2.
-Proof.
-  revert e1 e2; induction K => el er /=;
-     (move=><-; reflexivity) || (case => /IHK <-; reflexivity).
-Qed.
-
-Lemma fill_value K e v':
-  e2v (fill K e) = Some v' → is_Some (e2v e).
-Proof.
-  revert v'; induction K => v' /=; try discriminate;
-    try destruct (e2v (fill K e)); rewrite ?v2v; eauto.
-Qed.
+(** The stepping relation *)
+Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
+  | BetaS e1 e2 v2 σ :
+     to_val e2 = Some v2 →
+     head_step (App (Rec e1) e2) σ e1.[(Rec e1),e2/] σ None
+  | PlusS n1 n2 σ:
+     head_step (Plus (LitNat n1) (LitNat n2)) σ (LitNat (n1 + n2)) σ None
+  | LeTrueS n1 n2 σ :
+     n1 ≤ n2 →
+     head_step (Le (LitNat n1) (LitNat n2)) σ LitTrue σ None
+  | LeFalseS n1 n2 σ :
+     n1 > n2 →
+     head_step (Le (LitNat n1) (LitNat n2)) σ LitFalse σ None
+  | FstS e1 v1 e2 v2 σ :
+     to_val e1 = Some v1 → to_val e2 = Some v2 →
+     head_step (Fst (Pair e1 e2)) σ e1 σ None
+  | SndS e1 v1 e2 v2 σ :
+     to_val e1 = Some v1 → to_val e2 = Some v2 →
+     head_step (Snd (Pair e1 e2)) σ e2 σ None
+  | CaseLS e0 v0 e1 e2 σ :
+     to_val e0 = Some v0 →
+     head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ None
+  | CaseRS e0 v0 e1 e2 σ :
+     to_val e0 = Some v0 →
+     head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
+  | ForkS e σ:
+     head_step (Fork e) σ LitUnit σ (Some e)
+  | AllocS e v σ l :
+     to_val e = Some v → σ !! l = None →
+     head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
+  | LoadS l v σ :
+     σ !! l = Some v →
+     head_step (Load (Loc l)) σ (of_val v) σ None
+  | StoreS l e v σ :
+     to_val e = Some v → is_Some (σ !! l) →
+     head_step (Store (Loc l) e) σ LitUnit (<[l:=v]>σ) None
+  | CasFailS l e1 v1 e2 v2 vl σ :
+     to_val e1 = Some v1 → to_val e2 = Some v2 →
+     σ !! l = Some vl → vl ≠ v1 →
+     head_step (Cas (Loc l) e1 e2) σ LitFalse σ None
+  | CasSucS l e1 v1 e2 v2 σ :
+     to_val e1 = Some v1 → to_val e2 = Some v2 →
+     σ !! l = Some v1 →
+     head_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None.
 
-Lemma fill_not_value e K :
-  e2v e = None → e2v (fill K e) = None.
-Proof.
-  intros Hnval.  induction K =>/=; by rewrite ?v2v /= ?IHK /=.
-Qed.
+(** Atomic expressions *)
+Definition atomic (e: expr) :=
+  match e with
+  | Alloc e => is_Some (to_val e)
+  | Load e => is_Some (to_val e)
+  | Store e1 e2 => is_Some (to_val e1) ∧ is_Some (to_val e2)
+  | Cas e0 e1 e2 => is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2)
+  | _ => False
+  end.
 
-Lemma fill_not_value2 e K v :
-  e2v e = None → e2v (fill K e) = Some v -> False.
+(** Close reduction under evaluation contexts.
+We could potentially make this a generic construction. *)
+Inductive prim_step
+    (e1 : expr) (σ1 : state) (e2 : expr) (σ2: state) (ef: option expr) : Prop :=
+  Ectx_step (K : ectx) e1' e2' :
+    e1 = fill K e1' → e2 = fill K e2' →
+    head_step e1' σ1 e2' σ2 ef → prim_step e1 σ1 e2 σ2 ef.
+
+(** Basic properties about the language *)
+Lemma to_of_val v : to_val (of_val v) = Some v.
+Proof. by induction v; simplify_option_equality. Qed.
+Lemma of_to_val e v : to_val e = Some v → of_val v = e.
 Proof.
-  intros Hnval Hval. erewrite fill_not_value in Hval by assumption. discriminate.
+  revert v; induction e; intros; simplify_option_equality; auto with f_equal.
 Qed.
-
-Lemma comp_empty K K' :
-  EmptyCtx = comp_ctx K K' →
-  K = EmptyCtx ∧ K' = EmptyCtx.
+Instance: Injective (=) (=) of_val.
+Proof. by intros ?? Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
+Instance ectx_item_fill_inj Ki : Injective (=) (=) (ectx_item_fill Ki).
+Proof. destruct Ki; intros ???; simplify_equality'; auto with f_equal. Qed.
+Instance ectx_fill_inj K : Injective (=) (=) (fill K).
+Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
+Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
+Proof. revert e; induction K1; simpl; auto with f_equal. Qed.
+Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
 Proof.
-  destruct K; try discriminate.
-  destruct K'; try discriminate.
-  done.
+  intros [v' Hv']; revert v' Hv'.
+  induction K as [|[]]; intros; simplify_option_equality; eauto.
 Qed.
-
-(** The stepping relation *)
-Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
-| BetaS e1 e2 v2 σ (Hv2 : e2v e2 = Some v2):
-    prim_step (App (Rec e1) e2) σ e1.[(Rec e1),e2/] σ None
-| PlusS n1 n2 σ:
-    prim_step (Plus (LitNat n1) (LitNat n2)) σ (LitNat (n1 + n2)) σ None
-| LeTrueS n1 n2 σ (Hle : n1 ≤ n2):
-    prim_step (Le (LitNat n1) (LitNat n2)) σ LitTrue σ None
-| LeFalseS n1 n2 σ (Hle : n1 > n2):
-    prim_step (Le (LitNat n1) (LitNat n2)) σ LitFalse σ None
-| FstS e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2):
-    prim_step (Fst (Pair e1 e2)) σ e1 σ None
-| SndS e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2):
-    prim_step (Snd (Pair e1 e2)) σ e2 σ None
-| CaseLS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
-    prim_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ None
-| CaseRS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
-    prim_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
-| ForkS e σ:
-    prim_step (Fork e) σ LitUnit σ (Some e)
-| AllocS e v σ l (Hv : e2v e = Some v) (Hfresh : σ !! l = None):
-    prim_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
-| LoadS l v σ (Hlookup : σ !! l = Some v):
-    prim_step (Load (Loc l)) σ (v2e v) σ None
-| StoreS l e v σ (Hv : e2v e = Some v) (Halloc : is_Some (σ !! l)):
-    prim_step (Store (Loc l) e) σ LitUnit (<[l:=v]>σ) None
-| CasFailS l e1 v1 e2 v2 vl σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2)
-  (Hlookup : σ !! l = Some vl) (Hne : vl <> v1):
-    prim_step (Cas (Loc l) e1 e2) σ LitFalse σ None
-| CasSucS l e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2)
-  (Hlookup : σ !! l = Some v1):
-    prim_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None
-.
-
-Definition reducible e σ : Prop :=
-  ∃ e' σ' ef, prim_step e σ e' σ' ef.
-
-Lemma reducible_not_value e σ :
-  reducible e σ → e2v e = None.
+Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
+Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
+Lemma values_head_stuck e1 σ1 e2 σ2 ef :
+  head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+Proof. destruct 1; naive_solver. Qed.
+Lemma values_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+Proof. intros [??? -> -> ?]; eauto using fill_not_val, values_head_stuck. Qed.
+Lemma atomic_not_val e : atomic e → to_val e = None.
+Proof. destruct e; naive_solver. Qed.
+Lemma atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
 Proof.
-  intros (e' & σ' & ef & Hstep). destruct Hstep; simpl in *; reflexivity.
+  rewrite eq_None_not_Some.
+  destruct K as [|[]]; naive_solver eauto using fill_val.
 Qed.
-
-Definition stuck (e : expr) σ : Prop :=
-  ∀ K e', e = fill K e' → ~reducible e' σ.
-
-Lemma values_stuck v σ :
-  stuck (v2e v) σ.
+Lemma atomic_head_step e1 σ1 e2 σ2 ef :
+  atomic e1 → head_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
+Proof. destruct 2; simpl; rewrite ?to_of_val; naive_solver. Qed.
+Lemma atomic_step e1 σ1 e2 σ2 ef :
+  atomic e1 → prim_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
 Proof.
-  intros ?? Heq.
-  edestruct (fill_value K) as [v' Hv'].
-  { by rewrite <-Heq, v2v. }
-  clear -Hv' => Hred. apply reducible_not_value in Hred.
-  destruct (e2v e'); discriminate.
+  intros Hatomic [K e1' e2' -> -> Hstep].
+  assert (K = []) as -> by eauto 10 using atomic_fill, values_head_stuck.
+  naive_solver eauto using atomic_head_step.
 Qed.
-
-Section step_by_value.
-(* When something does a step, and another decomposition of the same
-     expression has a non-value e in the hole, then K is a left
-     sub-context of K' - in other words, e also contains the reducible
-     expression *)
-Lemma step_by_value {K K' e e' σ} :
-  fill K e = fill K' e' →
-  reducible e' σ →
-  e2v e = None →
-  ∃ K'', K' = comp_ctx K K''.
+Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
+  head_step (ectx_item_fill Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
+Proof. destruct Ki; inversion_clear 1; simplify_option_equality; eauto. Qed.
+Lemma fill_item_inj Ki1 Ki2 e1 e2 :
+  to_val e1 = None → to_val e2 = None →
+  ectx_item_fill Ki1 e1 = ectx_item_fill Ki2 e2 → Ki1 = Ki2.
 Proof.
-  Ltac bad_fill := intros; exfalso; subst;
-                   (eapply values_stuck; eassumption) ||
-                     (eapply fill_not_value2; first eassumption;
-                      try match goal with
-                        [ H : fill _ _ = _ |- _ ] => erewrite ->H
-                      end;
-                      by erewrite ?v2v).
-  Ltac bad_red   Hfill e' Hred := exfalso; destruct e';
-      try discriminate Hfill; [];
-      case: Hfill; intros; subst; destruct Hred as (e'' & σ'' & ef & Hstep);
-      inversion Hstep; done || (clear Hstep; subst;
-      eapply fill_not_value2; last (
-        try match goal with [ H : _ = fill _ _ |- _ ] => erewrite <-H end; simpl;
-        repeat match goal with [ H : e2v _ = _ |- _ ] =>
-          erewrite H; clear H; simpl
-        end
-      ); eassumption || done).
-  Ltac good IH := intros; subst; 
-    let K'' := fresh "K''" in edestruct IH as [K'' Hcomp]; first eassumption;
-    exists K''; by eauto using f_equal, f_equal2, f_equal3, v2e_inj.
-
-  intros Hfill Hred Hnval. 
-  revert K' Hfill; induction K=>K' /= Hfill;
-    first (now eexists; reflexivity);
-    (destruct K'; simpl;
-      (* The first case is: K' is EmpyCtx. *)
-      first (by bad_red Hfill e' Hred);
-      (* Many of the other cases result in contradicting equalities. *)
-      try discriminate Hfill;
-      (* The remaining cases are "compatible" contexts - that result in the same
-         head symbol of the expression.
-         Test whether the context als has the same head, and use the appropriate
-         tactic. *)
-      by match goal with
-      | [ |- exists x, ?C _ = ?C _ ] =>
-        case: Hfill; good IHK
-      | [ |- exists x, ?C _ _ = ?C _ _ ] =>
-        case: Hfill; good IHK
-      | [ |- exists x, ?C _ _ _ = ?C _ _ _ ] =>
-        case: Hfill; good IHK
-      | _ => case: Hfill; bad_fill
-      end).
+  destruct Ki1, Ki2; intros; try discriminate; simplify_equality';
+    repeat match goal with
+    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
+    end; auto.
 Qed.
-End step_by_value.
-
-(** Atomic expressions *)
-Definition atomic (e: expr) :=
-  match e with
-  | Alloc e => is_Some (e2v e)
-  | Load e => is_Some (e2v e)
-  | Store e1 e2 => is_Some (e2v e1) ∧ is_Some (e2v e2)
-  | Cas e0 e1 e2 => is_Some (e2v e0) ∧ is_Some (e2v e1) ∧ is_Some (e2v e2)
-  | _ => False
-  end.
-
-Lemma atomic_not_value e :
-  atomic e -> e2v e = None.
+(* When something does a step, and another decomposition of the same expression
+has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
+other words, [e] also contains the reducible expression *)
+Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
+  fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 ef →
+  K `prefix_of` K'.
 Proof.
-  destruct e; simpl; contradiction || reflexivity.
+  intros Hfill Hred Hnval; revert K' Hfill.
+  induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil.
+  destruct K' as [|Ki' K']; simplify_equality'.
+  { destruct (proj1 (eq_None_not_Some (to_val (fill K e1))));
+      eauto using fill_not_val, head_ctx_step_val. }
+  cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
+  eauto using fill_item_inj, values_head_stuck, fill_not_val.
 Qed.
-
-Lemma atomic_step e1 σ1 e2 σ2 ef :
-  atomic e1 →
-  prim_step e1 σ1 e2 σ2 ef →
-  is_Some (e2v e2).
+Lemma alloc_fresh e v σ :
+  let l := fresh (dom _ σ) in
+  to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
 Proof.
-  destruct e1; simpl; intros Hatomic Hstep; inversion Hstep;
-    try contradiction Hatomic; rewrite ?v2v /=; eexists; reflexivity.
+  by intros; apply AllocS, (not_elem_of_dom (D:=gset positive)), is_fresh.
 Qed.
-
-(* Atomics must not contain evaluation positions. *)
-Lemma atomic_fill e K :
-  atomic (fill K e) →
-  e2v e = None →
-  K = EmptyCtx.
+End heap_lang.
+
+(** Language *)
+Program Canonical Structure heap_lang : language := {|
+  expr := heap_lang.expr; val := heap_lang.val; state := heap_lang.state;
+  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
+  atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
+|}.
+Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
+  heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
+Global Instance heap_lang_ctx : CtxLanguage heap_lang heap_lang.ectx.
 Proof.
-  destruct K; simpl; first reflexivity; unfold is_Some; intros Hatomic Hnval;
-    exfalso; try assumption;
-    try (destruct_conjs; eapply fill_not_value2; eassumption).
+  split.
+  * eauto using heap_lang.fill_not_val.
+  * intros K ????? [K' e1' e2' Heq1 Heq2 Hstep].
+    by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2.
+  * intros K e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
+    destruct (heap_lang.step_by_val
+      K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
+    rewrite heap_lang.fill_app in Heq1; apply (injective _) in Heq1.
+    exists (fill K' e2''); rewrite heap_lang.fill_app; split; auto.
+    econstructor; eauto.
 Qed.
-
-(** Instantiate the Iris language interface. This closes reduction under
-    evaluation contexts.
-    We could potentially make this a generic construction. *)
-Section Language.
-
-  Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
-    ∃ K e1' e2', e1 = fill K e1' ∧ e2 = fill K e2' ∧
-                 prim_step e1' σ1 e2' σ2 ef.
-  Program Canonical Structure heap_lang : language := {|
-    language.expr := expr;
-    language.val := value;
-    language.state := state;
-    of_val := v2e;
-    to_val := e2v;
-    language.atomic := atomic;
-    language.prim_step := ectx_step;
-    to_of_val := v2v;
-    of_to_val := e2e;
-    language.atomic_not_value := atomic_not_value
-  |}.
-  Next Obligation.
-    intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2.
-    eapply fill_not_value. eapply reducible_not_value. do 3 eexists; eassumption.
-  Qed.
-  Next Obligation.
-    intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep).
-    subst. move: (Hatomic). rewrite (atomic_fill e1' K).
-    - rewrite !fill_empty. eauto using atomic_step.
-    - assumption.
-    - clear Hatomic. eapply reducible_not_value. do 3 eexists; eassumption.
-  Qed.
-
-  (** We can have bind with arbitrary evaluation contexts **)
-  Lemma fill_is_ctx K: is_ctx (fill K).
-  Proof.
-    split.
-    - intros ? Hnval. by eapply fill_not_value.
-    - intros ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
-      exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
-      split; last split; reflexivity || assumption.
-    - intros ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep).
-      destruct (step_by_value (σ:=σ1) Heq1) as [K' HeqK].
-      + do 3 eexists. eassumption.
-      + assumption.
-      + subst e2 K''. rewrite -fill_comp in Heq1. apply fill_inj_r in Heq1.
-        subst e1'. exists (fill K' e2''). split; first by rewrite -fill_comp.
-        do 3 eexists. split; last split; eassumption || reflexivity.
-  Qed.
-
-  Lemma prim_ectx_step e1 σ1 e2 σ2 ef :
-    reducible e1 σ1 →
-    ectx_step e1 σ1 e2 σ2 ef →
-    prim_step e1 σ1 e2 σ2 ef.
-  Proof.
-    intros Hred (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
-    destruct (@step_by_value K' EmptyCtx e1' e1 σ1) as [K'' [HK' HK'']%comp_empty].
-    - by rewrite fill_empty.
-    - done.
-    - eapply reducible_not_value. do 3 eexists; eassumption.
-    - subst K' K'' e1 e2. by rewrite !fill_empty.
-  Qed.
-
-End Language.
diff --git a/barrier/heap_lang_tactics.v b/barrier/heap_lang_tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..5a3f3d081d080d5d6b692fac930e4abe5cecf34c
--- /dev/null
+++ b/barrier/heap_lang_tactics.v
@@ -0,0 +1,72 @@
+Require Export barrier.heap_lang.
+Require Import prelude.fin_maps.
+Import heap_lang.
+
+Ltac inv_step :=
+  repeat match goal with
+  | _ => progress simplify_map_equality' (* simplify memory stuff *)
+  | H : to_val _ = Some _ |- _ => apply of_to_val in H
+  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
+  | H : prim_step _ _ _ _ _ |- _ => destruct H; subst
+  | H : _ = fill ?K ?e |- _ =>
+     destruct K as [|[]];
+     simpl in H; first [subst e|discriminate H|injection' H]
+     (* ensure that we make progress for each subgoal *)
+  | H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
+    apply values_head_stuck, (fill_not_val K) in H;
+    by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
+  | H : head_step ?e _ _ _ _ |- _ =>
+     try (is_var e; fail 1); (* inversion yields many goals if e is a variable
+     and can thus better be avoided. *)
+     inversion H; subst; clear H
+  end.
+
+Ltac reshape_expr e tac :=
+  let rec go K e :=
+  match e with
+  | _ => tac (reverse K) e
+  | App ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (AppRCtx v1 :: K) e2 | _ => go (AppLCtx e2 :: K) e1
+     end
+  | Plus ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (PlusRCtx v1 :: K) e2 | _ => go (PlusLCtx e2 :: K) e1
+     end
+  | Le ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (LeRCtx v1 :: K) e2 | _ => go (LeLCtx e2 :: K) e1
+     end
+  | Pair ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (PairRCtx v1 :: K) e2 | _ => go (PairLCtx e2 :: K) e1
+     end
+  | Fst ?e => go (FstCtx :: K) e
+  | Snd ?e => go (SndCtx :: K) e
+  | InjL ?e => go (InjLCtx :: K) e
+  | InjR ?e => go (InjRCtx :: K) e
+  | 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 => go (StoreLCtx e2 :: K) e1 || go (StoreRCtx e1 :: K) e2
+  | Cas ?e0 ?e1 ?e2 =>
+     lazymatch e0 with
+     | of_val ?v0 =>
+        lazymatch e1 with
+        | of_val ?v1 => go (CasRCtx v0 v1 :: K) e2
+        | _ => go (CasMCtx v0 e2 :: K) e1
+        end
+     | _ => go (CasLCtx e1 e2 :: K) e0
+     end
+  end in go (@nil ectx_item) e.
+
+Ltac do_step tac :=
+  try match goal with |- reducible _ _ => eexists _, _, _ end;
+  simpl;
+  match goal with
+  | |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
+     reshape_expr e1 ltac:(fun K e1' =>
+       eapply Ectx_step with K e1' _); [reflexivity|reflexivity|];
+       first [apply alloc_fresh|econstructor];
+       rewrite ?to_of_val; tac; fail
+  end.
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 704c29a9a4a753e1e71522a9009dd901ca1e0b18..cd947d259d06c31646b76b329be9661a1602f9f9 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -1,19 +1,21 @@
 Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre barrier.heap_lang.
+Require Export iris.weakestpre barrier.heap_lang_tactics.
 Import uPred.
+Import heap_lang.
+Local Hint Extern 0 (reducible _ _) => do_step ltac:(eauto 2).
 
 Section lifting.
 Context {Σ : iFunctor}.
 Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+Implicit Types Q : val → iProp heap_lang Σ.
+Implicit Types K : ectx.
 
 (** Bind. *)
 Lemma wp_bind {E e} K Q :
-  wp E e (λ v, wp E (fill K (v2e v)) Q) ⊑ wp E (fill K e) Q.
-Proof. apply (wp_bind (K:=fill K)), fill_is_ctx. Qed.
+  wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
+Proof. apply wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
-
 Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
   reducible e1 σ1 →
@@ -23,303 +25,176 @@ Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
   ⊑ wp E2 e1 Q.
 Proof.
   intros ? He Hsafe Hstep.
-  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
-  etransitivity; last eapply wp_lift_step with (σ2 := σ1)
-    (φ0 := λ e' σ' ef, ef = None ∧ φ e' σ'); last first.
-  - intros e2 σ2 ef Hstep'%prim_ectx_step; last done.
-    by apply Hstep.
-  - destruct Hsafe as (e' & σ' & ? & ?).
-    do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); eassumption.
-  - done.
-  - eassumption.
-  - apply pvs_mono. apply sep_mono; first done.
-    apply later_mono. apply forall_mono=>e2. apply forall_mono=>σ2.
-    apply forall_intro=>ef. apply wand_intro_l.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l; move=>[-> Hφ]. eapply const_intro_l; first eexact Hφ.
-    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
-    apply pvs_mono. rewrite right_id. done.
+  rewrite -(wp_lift_step E1 E2 (λ e' σ' ef, ef = None ∧ φ e' σ') _ _ σ1) //.
+  apply pvs_mono, sep_mono, later_mono; first done.
+  apply forall_mono=>e2; apply forall_mono=>σ2.
+  apply forall_intro=>ef; apply wand_intro_l.
+  rewrite always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ?] /=.
+  by rewrite const_equiv // left_id wand_elim_r right_id.
 Qed.
 
 (* TODO RJ: Figure out some better way to make the
    postcondition a predicate over a *location* *)
 Lemma wp_alloc_pst E σ e v Q :
-  e2v e = Some v →
-  (ownP σ ★ ▷(∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
+  to_val e = Some v →
+  (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
        ⊑ wp E (Alloc e) Q.
 Proof.
-  (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *)
-  intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None);
-    last first.
-  - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done.
-    rewrite Hv in Hvl. inversion_clear Hvl.
-    eexists; split_ands; done.
-  - set (l := fresh $ dom (gset loc) σ).
-    exists (Loc l), ((<[l:=v]>)σ), None. eapply AllocS; first done.
-    apply (not_elem_of_dom (D := gset loc)). apply is_fresh.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>σ2.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [l [-> [-> Hl]]].
-    rewrite (forall_elim l). eapply const_intro_l; first eexact Hl.
-    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
-    rewrite -wp_value'; done.
+  intros; set (φ e' σ' := ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
+  rewrite -(wp_lift_step E E φ _ _  σ) // /φ; last by intros; inv_step; eauto.
+  rewrite -pvs_intro. apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[l [-> [-> ?]]].
+  by rewrite (forall_elim l) const_equiv // left_id wand_elim_r -wp_value'.
 Qed.
-
 Lemma wp_load_pst E σ l v Q :
   σ !! l = Some v →
-  (ownP σ ★ ▷(ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
+  (ownP σ ★ ▷ (ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
 Proof.
-  intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first.
-  - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ}.
-    rewrite Hlookup. case=>->. done.
-  - do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>σ2.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value.
+  intros; rewrite -(wp_lift_step E E (λ e' σ', e' = of_val v ∧ σ' = σ)) //;
+    last by intros; inv_step; eauto.
+  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value.
 Qed.
-
 Lemma wp_store_pst E σ l e v v' Q :
-  e2v e = Some v →
-  σ !! l = Some v' →
-  (ownP σ ★ ▷(ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
+  to_val e = Some v → σ !! l = Some v' →
+  (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
 Proof.
-  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first.
-  - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ2}.
-    rewrite Hvl in Hv. inversion_clear Hv. done.
-  - do 3 eexists. eapply StoreS; last (eexists; eassumption). eassumption.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>σ2.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value'.
+  intros.
+  rewrite -(wp_lift_step E E (λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ)) //;
+    last by intros; inv_step; eauto.
+  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
-
 Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
-  e2v e1 = Some v1 → e2v e2 = Some v2 →
-  σ !! l = Some v' → v' <> v1 →
-  (ownP σ ★ ▷(ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
+  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
+  (ownP σ ★ ▷ (ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
-  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = LitFalse ∧ σ' = σ) (E1:=E); auto; last first.
-  - by inversion_clear 1; simplify_map_equality.
-  - do 3 eexists; econstructor; eauto.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2'. apply forall_intro=>σ2'.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value'.
+  intros; rewrite -(wp_lift_step E E (λ e' σ', e' = LitFalse ∧ σ' = σ)) //;
+    last by intros; inv_step; eauto.
+  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2'; apply forall_intro=>σ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
-
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
-  e2v e1 = Some v1 → e2v e2 = Some v2 →
-  σ !! l = Some v1 →
-  (ownP σ ★ ▷(ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
+  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
+  (ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
-  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ); last first.
-  - intros e2' σ2' ef Hstep. move:H. inversion_clear Hstep=>H.
-    (* FIXME this rewriting is rather ugly. *)
-    + exfalso. rewrite H in Hlookup. case:Hlookup=>?; subst vl.
-      rewrite Hvl in Hv1. case:Hv1=>?; subst v1. done.
-    + rewrite H in Hlookup. case:Hlookup=>?; subst v1.
-      rewrite Hl in Hv2. case:Hv2=>?; subst v2. done.
-  - do 3 eexists. eapply CasSucS; eassumption.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2'. apply forall_intro=>σ2'.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value'.
+  intros.
+  rewrite -(wp_lift_step E E (λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ)) //;
+    last by intros; inv_step; eauto.
+  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2'; apply forall_intro=>σ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
-
 Lemma wp_fork E e :
-  ▷ wp coPset_all e (λ _, True : iProp heap_lang Σ)
-  ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
+  ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
 Proof.
-  etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e' ef, e' = LitUnit ∧ ef = Some e);
-    last first.
-  - intros σ1 e2 σ2 ef Hstep%prim_ectx_step; last first.
-    { do 3 eexists. eapply ForkS. }
-    inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); [].
-    eapply ForkS.
-  - reflexivity.
-  - apply later_mono.
-    apply forall_intro=>e2; apply forall_intro=>ef.
-    apply impl_intro_l, const_elim_l=>-[-> ->] /=; apply sep_intro_True_l; auto.
-    by rewrite -wp_value' //; apply const_intro.
+  rewrite -(wp_lift_pure_step E (λ e' ef, e' = LitUnit ∧ ef = Some e)) //=;
+    last by intros; inv_step; eauto.
+  apply later_mono, forall_intro=>e2; apply forall_intro=>ef.
+  apply impl_intro_l, const_elim_l=>-[-> ->] /=.
+  apply sep_intro_True_l; last done.
+  by rewrite -wp_value' //; apply const_intro.
 Qed.
-
 Lemma wp_lift_pure_step E (φ : expr → Prop) Q e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ ef = None ∧ φ e2) →
   (▷ ∀ e2, ■ φ e2 → wp E e2 Q) ⊑ wp E e1 Q.
 Proof.
-  intros He Hsafe Hstep.
-  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
-  etransitivity; last eapply wp_lift_pure_step with
-    (φ0 := λ e' ef, ef = None ∧ φ e'); last first.
-  - intros σ1 e2 σ2 ef Hstep'%prim_ectx_step; last done.
-    by apply Hstep.
-  - intros σ1. destruct (Hsafe σ1) as (e' & σ' & ? & ?).
-    do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); eassumption.
-  - done.
-  - apply later_mono. apply forall_mono=>e2. apply forall_intro=>ef.
-    apply impl_intro_l. apply const_elim_l; move=>[-> Hφ].
-    eapply const_intro_l; first eexact Hφ. rewrite impl_elim_r.
-    rewrite right_id. done.
+  intros; rewrite -(wp_lift_pure_step E (λ e' ef, ef = None ∧ φ e')) //=.
+  apply later_mono, forall_mono=>e2; apply forall_intro=>ef.
+  apply impl_intro_l, const_elim_l=>-[-> ?] /=.
+  by rewrite const_equiv // left_id right_id.
 Qed.
-
 Lemma wp_rec E ef e v Q :
-  e2v e = Some v →
-  ▷wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
+  to_val e = Some v →
+  ▷ wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
 Proof.
-  etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = ef.[Rec ef, e /]); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. eapply BetaS; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->. done.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = ef.[Rec ef, e /])
+    Q (App (Rec ef) e)) //=; last by intros; inv_step; eauto.
+  by apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
 Qed.
-
-Lemma wp_plus n1 n2 E Q :
-  ▷Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
+Lemma wp_plus E n1 n2 Q :
+  ▷ Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
-  etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = LitNat (n1 + n2)); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last reflexivity; done.
+  rewrite -(wp_lift_pure_step E (λ e', e' = LitNat (n1 + n2))) //=;
+    last by intros; inv_step; eauto.
+  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
-Lemma wp_le_true n1 n2 E Q :
+Lemma wp_le_true E n1 n2 Q :
   n1 ≤ n2 →
-  ▷Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
+  ▷ Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros Hle. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = LitTrue); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; first done.
-    exfalso. eapply le_not_gt with (n := n1); eassumption.
-  - intros ?. do 3 eexists. econstructor; done.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last reflexivity; done.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = LitTrue)) //=;
+    last by intros; inv_step; eauto with lia.
+  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
-Lemma wp_le_false n1 n2 E Q :
+Lemma wp_le_false E n1 n2 Q :
   n1 > n2 →
-  ▷Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
+  ▷ Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros Hle. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = LitFalse); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; last done.
-    exfalso. eapply le_not_gt with (n := n1); eassumption.
-  - intros ?. do 3 eexists. econstructor; done.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last reflexivity; done.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = LitFalse)) //=;
+    last by intros; inv_step; eauto with lia.
+  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
-Lemma wp_fst e1 v1 e2 v2 E Q :
-  e2v e1 = Some v1 → e2v e2 = Some v2 →
+Lemma wp_fst E e1 v1 e2 v2 Q :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q.
 Proof.
-  intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = e1); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last eassumption; done.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e1)) //=;
+    last by intros; inv_step; eauto.
+  apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
-Lemma wp_snd e1 v1 e2 v2 E Q :
-  e2v e1 = Some v1 → e2v e2 = Some v2 →
-  ▷Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
+Lemma wp_snd E e1 v1 e2 v2 Q :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  ▷ Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
 Proof.
-  intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = e2); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last eassumption; done.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e2)) //=;
+    last by intros; inv_step; eauto.
+  apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
-Lemma wp_case_inl e0 v0 e1 e2 E Q :
-  e2v e0 = Some v0 →
-  ▷wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
+Lemma wp_case_inl E e0 v0 e1 e2 Q :
+  to_val e0 = Some v0 →
+  ▷ wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
 Proof.
-  intros Hv0. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = e1.[e0/]); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e1'. apply impl_intro_l.
-    by apply const_elim_l=>->.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e1.[e0/]) _
+    (Case (InjL e0) e1 e2)) //=; last by intros; inv_step; eauto.
+  by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
 Qed.
-
-Lemma wp_case_inr e0 v0 e1 e2 E Q :
-  e2v e0 = Some v0 →
-  ▷wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
+Lemma wp_case_inr E e0 v0 e1 e2 Q :
+  to_val e0 = Some v0 →
+  ▷ wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
 Proof.
-  intros Hv0. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = e2.[e0/]); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
-    by apply const_elim_l=>->.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e2.[e0/]) _
+    (Case (InjR e0) e1 e2)) //=; last by intros; inv_step; eauto.
+  by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
 Qed.
 
 (** Some derived stateless axioms *)
-
-Lemma wp_le n1 n2 E P Q :
-  (n1 ≤ n2 → P ⊑ ▷Q LitTrueV) →
-  (n1 > n2 → P ⊑ ▷Q LitFalseV) →
+Lemma wp_le E n1 n2 P Q :
+  (n1 ≤ n2 → P ⊑ ▷ Q LitTrueV) →
+  (n1 > n2 → P ⊑ ▷ Q LitFalseV) →
   P ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros HPle HPgt.
-  assert (Decision (n1 ≤ n2)) as Hn12 by apply _.
-  destruct Hn12 as [Hle|Hgt].
-  - rewrite -wp_le_true; auto.
-  - assert (n1 > n2) by omega. rewrite -wp_le_false; auto.
+  intros; destruct (decide (n1 ≤ n2)).
+  * rewrite -wp_le_true; auto.
+  * rewrite -wp_le_false; auto with lia.
 Qed.
 End lifting.
diff --git a/barrier/sugar.v b/barrier/sugar.v
index d8fe3920f7050bc84ec8273341b3846ef15dc517..92869fe6990c15df9386c3491ca53619eab5bdce 100644
--- a/barrier/sugar.v
+++ b/barrier/sugar.v
@@ -1,5 +1,6 @@
 Require Export barrier.heap_lang barrier.lifting.
 Import uPred.
+Import heap_lang.
 
 (** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
 Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
@@ -13,67 +14,52 @@ Definition Eq e1 e2 :=
 
 Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
 
-Definition LetCtx (K1 : ectx) (e2 : {bind expr}) := AppRCtx (LamV e2) K1.
-Definition SeqCtx (K1 : ectx) (e2 : expr) := LetCtx K1 (e2.[ren(+1)]).
+Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2).
+Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
 
 Section suger.
 Context {Σ : iFunctor}.
 Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+Implicit Types Q : val → iProp heap_lang Σ.
 
 (** Proof rules for the sugar *)
 Lemma wp_lam E ef e v Q :
-  e2v e = Some v → ▷wp E ef.[e/] Q ⊑ wp E (App (Lam ef) e) Q.
+  to_val e = Some v → ▷ wp E ef.[e/] Q ⊑ wp E (App (Lam ef) e) Q.
 Proof.
   intros Hv. rewrite -wp_rec; last eassumption.
   (* RJ: This pulls in functional extensionality. If that bothers us, we have
      to talk to the Autosubst guys. *)
   by asimpl.
 Qed.
-
-Lemma wp_let e1 e2 E Q :
-  wp E e1 (λ v, ▷wp E (e2.[v2e v/]) Q) ⊑ wp E (Let e1 e2) Q.
+Lemma wp_let E e1 e2 Q :
+  wp E e1 (λ v, ▷wp E (e2.[of_val v/]) Q) ⊑ wp E (Let e1 e2) Q.
 Proof.
-  rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v.
-  rewrite -wp_lam //. by rewrite v2v.
+  rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v.
+  by rewrite -wp_lam //= to_of_val.
 Qed.
-
-Lemma wp_if_true e1 e2 E Q :
-  ▷wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q.
-Proof.
-  rewrite -wp_case_inl //. by asimpl.
-Qed.
-
-Lemma wp_if_false e1 e2 E Q :
-  ▷wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q.
-Proof.
-  rewrite -wp_case_inr //. by asimpl.
-Qed.
-
-Lemma wp_lt n1 n2 E P Q :
-  (n1 < n2 → P ⊑ ▷Q LitTrueV) →
-  (n1 ≥ n2 → P ⊑ ▷Q LitFalseV) →
+Lemma wp_if_true E e1 e2 Q : ▷ wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q.
+Proof. rewrite -wp_case_inl //. by asimpl. Qed.
+Lemma wp_if_false E e1 e2 Q : ▷ wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q.
+Proof. rewrite -wp_case_inr //. by asimpl. Qed.
+Lemma wp_lt E n1 n2 P Q :
+  (n1 < n2 → P ⊑ ▷ Q LitTrueV) →
+  (n1 ≥ n2 → P ⊑ ▷ Q LitFalseV) →
   P ⊑ wp E (Lt (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros HPlt HPge.
-  rewrite -(wp_bind (LeLCtx EmptyCtx _)) -wp_plus -later_intro. simpl.
-  apply wp_le; intros; [apply HPlt|apply HPge]; omega.
+  intros; rewrite -(wp_bind [LeLCtx _]) -wp_plus -later_intro /=.
+  auto using wp_le with lia.
 Qed.
-
-Lemma wp_eq n1 n2 E P Q :
-  (n1 = n2 → P ⊑ ▷Q LitTrueV) →
-  (n1 ≠ n2 → P ⊑ ▷Q LitFalseV) →
+Lemma wp_eq E n1 n2 P Q :
+  (n1 = n2 → P ⊑ ▷ Q LitTrueV) →
+  (n1 ≠ n2 → P ⊑ ▷ Q LitFalseV) →
   P ⊑ wp E (Eq (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros HPeq HPne.
-  rewrite -wp_let -wp_value' // -later_intro. asimpl.
-  rewrite -wp_rec //. asimpl.
-  rewrite -(wp_bind (CaseCtx EmptyCtx _ _)) -later_intro.
-  apply wp_le; intros Hn12.
-  - asimpl. rewrite -wp_case_inl // -!later_intro. apply wp_le; intros Hn12'.
-    + apply HPeq; omega.
-    + apply HPne; omega.
-  - asimpl. rewrite -wp_case_inr // -later_intro -wp_value' //.
-    apply HPne; omega.
+  rewrite -wp_let -wp_value' // -later_intro; asimpl.
+  rewrite -wp_rec //; asimpl.
+  rewrite -(wp_bind [CaseCtx _ _]) -later_intro; asimpl.
+  apply wp_le; intros; asimpl.
+  * rewrite -wp_case_inl // -!later_intro. apply wp_le; auto with lia.
+  * rewrite -wp_case_inr // -later_intro -wp_value' //; auto with lia.
 Qed.
 End suger.
diff --git a/barrier/tests.v b/barrier/tests.v
index fa6c63b041f4f735a009911d28eec901dfdc4838..4f0107b6d36a74f261c26a576140f2e1d88212c3 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -1,34 +1,26 @@
 (** This file is essentially a bunch of testcases. *)
 Require Import modures.logic.
 Require Import barrier.lifting barrier.sugar.
+Import heap_lang.
 Import uPred.
 
 Module LangTests.
-  Definition add :=  Plus (LitNat 21) (LitNat 21).
+  Definition add := Plus (LitNat 21) (LitNat 21).
   Goal ∀ σ, prim_step add σ (LitNat 42) σ None.
-  Proof.
-    constructor.
-  Qed.
-
+  Proof. intros; do_step done. Qed.
   Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
   Definition rec_app := App rec (LitNat 0).
   Goal ∀ σ, prim_step rec_app σ rec_app σ None.
-  Proof.
-    move=>?. eapply BetaS.
-    reflexivity.
-  Qed.
-
+  Proof. intros; do_step done. Qed.
   Definition lam := Lam (Plus (Var 0) (LitNat 21)).
   Goal ∀ σ, prim_step (App lam (LitNat 21)) σ add σ None.
-  Proof.
-    move=>?. eapply BetaS. reflexivity.
-  Qed.
+  Proof. intros; do_step done. Qed.
 End LangTests.
 
 Module LiftingTests.
   Context {Σ : iFunctor}.
   Implicit Types P : iProp heap_lang Σ.
-  Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+  Implicit Types Q : val → iProp heap_lang Σ.
 
   (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
   Definition e3 := Load (Var 0).
@@ -42,26 +34,24 @@ Module LiftingTests.
     rewrite -later_intro. apply forall_intro=>l.
     apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
     rewrite -later_intro. asimpl.
-    rewrite -(wp_bind (SeqCtx EmptyCtx (Load (Loc _)))).
-    rewrite -(wp_bind (StoreRCtx (LocV _) EmptyCtx)).
-    rewrite -(wp_bind (PlusLCtx EmptyCtx _)).
+    rewrite -(wp_bind [SeqCtx (Load (Loc _))]).
+    rewrite -(wp_bind [StoreRCtx (LocV _)]).
+    rewrite -(wp_bind [PlusLCtx _]).
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
-    { apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
+    { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     rewrite -wp_plus -later_intro.
     rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
-    { apply: lookup_insert. }
-    { reflexivity. }
+    { by rewrite lookup_insert. }
+    { done. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     rewrite -wp_lam // -later_intro. asimpl.
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
-    { apply: lookup_insert. }
+    { by rewrite lookup_insert. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     by apply const_intro.
   Qed.
 
-  Import Nat.
-
   Definition FindPred' n1 Sn1 n2 f := If (Lt Sn1 n2)
                                       (App f Sn1)
                                       n1.
@@ -83,12 +73,12 @@ Module LiftingTests.
     { apply and_mono; first done. by rewrite -later_intro. }
     apply later_mono.
     (* Go on. *)
-    rewrite -(wp_let _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
+    rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
     rewrite -wp_plus. asimpl.
-    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
-    rewrite -!later_intro. simpl.
+    rewrite -(wp_bind [CaseCtx _ _]).
+    rewrite -!later_intro /=.
     apply wp_lt; intros Hn12.
-    - (* TODO RJ: It would be better if we could use wp_if_true here
+    * (* TODO RJ: It would be better if we could use wp_if_true here
          (and below). But we cannot, because the substitutions in there
          got already unfolded. *)
       rewrite -wp_case_inl //.
@@ -97,30 +87,29 @@ Module LiftingTests.
       eapply impl_elim; first by eapply and_elim_l. apply and_intro.
       + apply const_intro; omega.
       + by rewrite !and_elim_r.
-    - rewrite -wp_case_inr //.
+    * rewrite -wp_case_inr //.
       rewrite -!later_intro -wp_value' //.
       rewrite and_elim_r. apply const_elim_l=>Hle.
-      assert (Heq: n1 = pred n2) by omega. by subst n1.
+      by replace n1 with (pred n2) by lia.
   Qed.
 
   Lemma Pred_spec n E Q :
     ▷Q (LitNatV $ pred n) ⊑ wp E (App Pred (LitNat n)) Q.
   Proof.
     rewrite -wp_lam //. asimpl.
-    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
-    apply later_mono, wp_le; intros Hn.
+    rewrite -(wp_bind [CaseCtx _ _]).
+    apply later_mono, wp_le=> Hn.
     - rewrite -wp_case_inl //.
       rewrite -!later_intro -wp_value' //.
-      assert (Heq: n = 0) by omega. by subst n.
+      by replace n with 0 by lia.
     - rewrite -wp_case_inr //.
-      rewrite -!later_intro -FindPred_spec. apply and_intro.
-      + by apply const_intro; omega.
-      + done.
+      rewrite -!later_intro -FindPred_spec.
+      auto using and_intro, const_intro with lia.
   Qed.
 
   Goal ∀ E,
-    (True : iProp heap_lang Σ)
-    ⊑ wp E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
+    True ⊑ wp (Σ:=Σ) E
+      (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
   Proof.
     intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
     asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
diff --git a/iris/hoare.v b/iris/hoare.v
index edfc9e54f9e8068f2fe32a20be73aea776db7cef..a54afed2f3e406f975a168bc0feb99170c2851f8 100644
--- a/iris/hoare.v
+++ b/iris/hoare.v
@@ -57,9 +57,9 @@ Proof.
   rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
   rewrite (forall_elim v) pvs_impl_r -(pvs_intro E1) pvs_trans; solve_elem_of.
 Qed.
-Lemma ht_bind `(HK : is_ctx K) E P Q Q' e :
-  ({{ P }} e @ E {{ Q }} ∧ ∀ v, {{ Q v }} K (of_val v) @ E {{ Q' }})
-  ⊑ {{ P }} K e @ E {{ Q' }}.
+Lemma ht_bind `{CtxLanguage Λ C} K E P Q Q' e :
+  ({{ P }} e @ E {{ Q }} ∧ ∀ v, {{ Q v }} fill K (of_val v) @ E {{ Q' }})
+  ⊑ {{ P }} fill K e @ E {{ Q' }}.
 Proof.
   intros; apply (always_intro' _ _), impl_intro_l.
   rewrite (associative _ P) {1}/ht always_elim impl_elim_r.
diff --git a/iris/hoare_lifting.v b/iris/hoare_lifting.v
index 5e5467f1bf64845cbabbc80207557367d4f3c045..7bfd02e2731567e931ce744b272dce15d9d0e818 100644
--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -55,7 +55,7 @@ Proof.
   rewrite -(ht_lift_step E E φ'  _ P
     (λ e2 σ2 ef, ownP σ2 ★ ■ (φ' e2 σ2 ef))%I
     (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I);
-    try by (rewrite /φ'; eauto using atomic_not_value, atomic_step).
+    try by (rewrite /φ'; eauto using atomic_not_val, atomic_step).
   apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
   apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
   apply and_intro; [|apply and_intro; [|done]].
diff --git a/iris/language.v b/iris/language.v
index 9bb0fca56ebfd3a6092dd85cd768831d782e10ac..035062d938698dd09677529b414e7047b465bf2c 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -11,7 +11,7 @@ Structure language := Language {
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
   values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None;
-  atomic_not_value e : atomic e → to_val e = None;
+  atomic_not_val e : atomic e → to_val e = None;
   atomic_step e1 σ1 e2 σ2 ef :
     atomic e1 →
     prim_step e1 σ1 e2 σ2 ef →
@@ -24,7 +24,7 @@ Arguments prim_step {_} _ _ _ _ _.
 Arguments to_of_val {_} _.
 Arguments of_to_val {_} _ _ _.
 Arguments values_stuck {_} _ _ _ _ _ _.
-Arguments atomic_not_value {_} _ _.
+Arguments atomic_not_val {_} _ _.
 Arguments atomic_step {_} _ _ _ _ _ _ _.
 
 Canonical Structure istateC Σ := leibnizC (state Σ).
@@ -47,19 +47,22 @@ Section language.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
   Lemma atomic_of_val v : ¬atomic (of_val v).
-  Proof.
-    by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
-  Qed.
+  Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed.
   Global Instance: Injective (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
-
-  Record is_ctx (K : expr Λ → expr Λ) := IsCtx {
-    is_ctx_value e : to_val e = None → to_val (K e) = None;
-    is_ctx_step_preserved e1 σ1 e2 σ2 ef :
-      prim_step e1 σ1 e2 σ2 ef → prim_step (K e1) σ1 (K e2) σ2 ef;
-    is_ctx_step e1' σ1 e2 σ2 ef :
-      to_val e1' = None → prim_step (K e1') σ1 e2 σ2 ef →
-      ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 ef
-  }.
 End language.
 
+Class Fill C E := fill : C → E → E.
+Instance: Params (@fill) 3.
+Arguments fill {_ _ _} !_ _ / : simpl nomatch.
+
+Class CtxLanguage (Λ : language) (C : Type) `{Fill C (expr Λ)} := {
+  fill_not_val K e :
+    to_val e = None → to_val (fill K e) = None;
+  fill_step K e1 σ1 e2 σ2 ef :
+    prim_step e1 σ1 e2 σ2 ef →
+    prim_step (fill K e1) σ1 (fill K e2) σ2 ef;
+  fill_step_inv K e1' σ1 e2 σ2 ef :
+    to_val e1' = None → prim_step (fill K e1') σ1 e2 σ2 ef →
+    ∃ e2', e2 = fill K e2' ∧ prim_step e1' σ1 e2' σ2 ef
+}.
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index 8acb0c293e52bf5418b902ff8bf7b240a0a2e66e..a396c92fdac4737a0ca2d3f7ddf0789756b6ec1f 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -117,7 +117,7 @@ Qed.
 Lemma wp_atomic E1 E2 e Q :
   E2 ⊆ E1 → atomic e → pvs E1 E2 (wp E2 e (λ v, pvs E2 E1 (Q v))) ⊑ wp E1 e Q.
 Proof.
-  intros ? He r n ? Hvs; constructor; eauto using atomic_not_value.
+  intros ? He r n ? Hvs; constructor; eauto using atomic_not_val.
   intros rf k Ef σ1 ???.
   destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
   inversion Hwp as [|???? Hgo]; subst; [by destruct (atomic_of_val v)|].
@@ -161,17 +161,17 @@ Proof.
   * apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
     eapply uPred_weaken with rR n; eauto.
 Qed.
-Lemma wp_bind `(HK : is_ctx K) E e Q :
-  wp E e (λ v, wp E (K (of_val v)) Q) ⊑ wp E (K e) Q.
+Lemma wp_bind `{CtxLanguage Λ C} E K e Q :
+  wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
 Proof.
   intros r n; revert e r; induction n as [n IH] using lt_wf_ind; intros e r ?.
-  destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using is_ctx_value.
+  destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using fill_not_val.
   intros rf k Ef σ1 ???; destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
   split.
   { destruct Hsafe as (e2&σ2&ef&?).
-    by exists (K e2), σ2, ef; apply is_ctx_step_preserved. }
+    by exists (fill K e2), σ2, ef; apply fill_step. }
   intros e2 σ2 ef ?.
-  destruct (is_ctx_step _ HK e σ1 e2 σ2 ef) as (e2'&->&?); auto.
+  destruct (fill_step_inv K e σ1 e2 σ2 ef) as (e2'&->&?); auto.
   destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto.
   exists r2, r2'; split_ands; try eapply IH; eauto.
 Qed.
diff --git a/modures/logic.v b/modures/logic.v
index f14b3da45bcddbe047795b83f633f7ae954c549f..a50c0dbc344506883ae80b45a0249ff6acea0fb7 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -453,6 +453,8 @@ Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
 Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■ φ) ⊑ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
+Lemma const_equiv (φ : Prop) : φ → (■ φ : uPred M)%I ≡ True%I.
+Proof. intros; apply (anti_symmetric _); auto using const_intro. Qed.
 Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
 Proof. intros ->; apply eq_refl. Qed.
 Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a).
@@ -524,6 +526,12 @@ Global Instance or_comm : Commutative (≡) (@uPred_or M).
 Proof. intros P Q; apply (anti_symmetric (⊑)); auto. Qed.
 Global Instance or_assoc : Associative (≡) (@uPred_or M).
 Proof. intros P Q R; apply (anti_symmetric (⊑)); auto. Qed.
+Global Instance True_impl : LeftId (≡) True%I (@uPred_impl M).
+Proof.
+  intros P; apply (anti_symmetric (⊑)).
+  * by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
+  * by apply impl_intro_l; rewrite left_id.
+Qed.
 Lemma or_and_l P Q R : (P ∨ Q ∧ R)%I ≡ ((P ∨ Q) ∧ (P ∨ R))%I.
 Proof.
   apply (anti_symmetric (⊑)); first auto.