diff --git a/algebra/agree.v b/algebra/agree.v
index a62b288f26eaad80b7dc805c42eba32bdddfcb69..a85d59e8f795968981919624de76fdc98b47ae0c 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import upred.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
-  agree_car :> nat → A;
+  agree_car : nat → A;
   agree_is_valid : nat → Prop;
   agree_valid_S n : agree_is_valid (S n) → agree_is_valid n
 }.
@@ -15,7 +15,7 @@ Section agree.
 Context {A : cofeT}.
 
 Instance agree_validN : ValidN (agree A) := λ n x,
-  agree_is_valid x n ∧ ∀ n', n' ≤ n → x n ≡{n'}≡ x n'.
+  agree_is_valid x n ∧ ∀ n', n' ≤ n → agree_car x n ≡{n'}≡ agree_car x n'.
 Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
 
 Lemma agree_valid_le n n' (x : agree A) :
@@ -24,12 +24,13 @@ Proof. induction 2; eauto using agree_valid_S. Qed.
 
 Instance agree_equiv : Equiv (agree A) := λ x y,
   (∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧
-  (∀ n, agree_is_valid x n → x n ≡{n}≡ y n).
+  (∀ n, agree_is_valid x n → agree_car x n ≡{n}≡ agree_car y n).
 Instance agree_dist : Dist (agree A) := λ n x y,
   (∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧
-  (∀ n', n' ≤ n → agree_is_valid x n' → x n' ≡{n'}≡ y n').
+  (∀ n', n' ≤ n → agree_is_valid x n' → agree_car x n' ≡{n'}≡ agree_car y n').
 Program Instance agree_compl : Compl (agree A) := λ c,
-  {| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}.
+  {| agree_car n := agree_car (c n) n;
+     agree_is_valid n := agree_is_valid (c n) n |}.
 Next Obligation.
   intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto.
 Qed.
@@ -44,20 +45,15 @@ Proof.
     + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
     + intros x y z Hxy Hyz; split; intros n'; intros.
       * trans (agree_is_valid y n'). by apply Hxy. by apply Hyz.
-      * trans (y n'). by apply Hxy. by apply Hyz, Hxy.
+      * trans (agree_car y n'). by apply Hxy. by apply Hyz, Hxy.
   - intros n x y Hxy; split; intros; apply Hxy; auto.
   - intros n c; apply and_wlog_r; intros;
       symmetry; apply (chain_cauchy c); naive_solver.
 Qed.
 Canonical Structure agreeC := CofeT (agree A) agree_cofe_mixin.
 
-Lemma agree_car_ne n (x y : agree A) : ✓{n} x → x ≡{n}≡ y → x n ≡{n}≡ y n.
-Proof. by intros [??] Hxy; apply Hxy. Qed.
-Lemma agree_cauchy n (x : agree A) i : ✓{n} x → i ≤ n → x n ≡{i}≡ x i.
-Proof. by intros [? Hx]; apply Hx. Qed.
-
 Program Instance agree_op : Op (agree A) := λ x y,
-  {| agree_car := x;
+  {| agree_car := agree_car x;
      agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ≡{n}≡ y |}.
 Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
 Instance agree_pcore : PCore (agree A) := Some.
@@ -127,13 +123,19 @@ Proof. by constructor. Qed.
 Program Definition to_agree (x : A) : agree A :=
   {| agree_car n := x; agree_is_valid n := True |}.
 Solve Obligations with done.
+
 Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
 Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
 Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
+
 Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree).
 Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
-Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
-Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
+
+Lemma to_agree_uninj n (x : agree A) : ✓{n} x → ∃ y : A, to_agree y ≡{n}≡ x.
+Proof.
+  intros [??]. exists (agree_car x n).
+  split; naive_solver eauto using agree_valid_le.
+Qed.
 
 (** Internalized properties *)
 Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M).
@@ -148,7 +150,7 @@ Arguments agreeC : clear implicits.
 Arguments agreeR : clear implicits.
 
 Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
-  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x;
+  {| agree_car n := f (agree_car x n); agree_is_valid := agree_is_valid x;
      agree_valid_S := agree_valid_S _ x |}.
 Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
 Proof. by destruct x. Qed.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index ab73d1368fd7b7fd7b8948c6137aba74a245dc77..65de4c44875bb15a58ad31bfb256a225b92706c6 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -153,12 +153,12 @@ Section heap.
     to_val e = Some v → nclose heapN ⊆ E →
     heap_ctx ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
-    iIntros (??) "[#Hinv HΦ]". rewrite /heap_ctx.
+    iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
     iPvs (auth_empty heap_name) as "Hheap".
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hinv Hheap". iIntros (h). rewrite left_id.
     iIntros "[% Hheap]". rewrite /heap_inv.
-    iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
+    iApply wp_alloc_pst. iFrame "Hheap". iNext.
     iIntros (l) "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
     rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
     iFrame "Hheap". iSplitR; first iPureIntro.
@@ -173,7 +173,7 @@ Section heap.
   Proof.
     iIntros (?) "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
     rewrite of_heap_singleton_op //. iFrame "Hl".
@@ -186,9 +186,9 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
-    iIntros (??) "[#Hh [Hl HΦ]]".
+    iIntros (<-%of_to_val ?) "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
@@ -202,9 +202,9 @@ Section heap.
     heap_ctx ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (????) "[#Hh [Hl HΦ]]".
+    iIntros (<-%of_to_val <-%of_to_val ??) "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite of_heap_singleton_op //. iFrame "Hl".
@@ -217,9 +217,9 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (???) "[#Hh [Hl HΦ]]".
+    iIntros (<-%of_to_val <-%of_to_val ?) "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 4ef1e428c0ea7269904e405c0c5719aed5b83154..881e486cc2d0b59fc0da2ec654792352496b8ab6 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -273,19 +273,6 @@ Inductive head_step : expr → state → expr → state → option (expr) → Pr
      σ !! l = Some v1 →
      head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
 
-(** 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)
-  (* Make "skip" atomic *)
-  | App (Rec _ _ (Lit _)) (Lit _) => True
-  | _ => False
-  end.
-
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
 Proof.
@@ -310,22 +297,6 @@ Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 Lemma val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
-Lemma atomic_not_val e : atomic e → to_val e = None.
-Proof. by destruct e. Qed.
-
-Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
-Proof.
-  intros. destruct Ki; simplify_eq/=; destruct_and?;
-    repeat (simpl || case_match || contradiction); eauto.
-Qed.
-
-Lemma atomic_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; try by eauto. subst.
-  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
-Qed.
-
 Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
   head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
 Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
@@ -391,13 +362,11 @@ Program Instance heap_ectxi_lang :
   EctxiLanguage
     (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
   of_val := heap_lang.of_val; to_val := heap_lang.to_val;
-  fill_item := heap_lang.fill_item;
-  atomic := heap_lang.atomic; head_step := heap_lang.head_step;
+  fill_item := heap_lang.fill_item; head_step := heap_lang.head_step
 |}.
 Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
-  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
-  heap_lang.fill_item_val, heap_lang.atomic_fill_item,
-  heap_lang.fill_item_no_val_inj, heap_lang.head_ctx_step_val.
+  heap_lang.val_stuck, heap_lang.fill_item_val, heap_lang.fill_item_no_val_inj,
+  heap_lang.head_ctx_step_val.
 
 Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index b6770446c51de7c40da227d411852fd9b6f1bf86..24eb4d3a6c6fe8c986870c08711745eea10f24e1 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -23,13 +23,12 @@ Lemma wp_bindi {E e} Ki Φ :
 Proof. exact: weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ e v Φ :
-  to_val e = Some v →
+Lemma wp_alloc_pst E σ v Φ :
   ▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) ={E}=★ Φ (LitV (LitLoc l)))
-  ⊢ WP Alloc e @ E {{ Φ }}.
+  ⊢ WP Alloc (of_val v) @ E {{ Φ }}.
 Proof.
-  iIntros (?)  "[HP HΦ]".
-  iApply (wp_lift_atomic_head_step (Alloc e) σ); try (by simpl; eauto).
+  iIntros "[HP HΦ]".
+  iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto with fsaV.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
   subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
@@ -40,36 +39,37 @@ Lemma wp_load_pst E σ l v Φ :
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
-    last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto.
+    last (by intros; inv_head_step; eauto using to_of_val). solve_atomic.
 Qed.
 
-Lemma wp_store_pst E σ l e v v' Φ :
-  to_val e = Some v → σ !! l = Some v' →
+Lemma wp_store_pst E σ l v v' Φ :
+  σ !! l = Some v' →
   ▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) ={E}=★ Φ (LitV LitUnit))
-  ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
+  ⊢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
 Proof.
-  intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
-    ?right_id //; last (by intros; inv_head_step; eauto); simpl; by eauto.
+  intros ?.
+  rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
+    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
-Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
+Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
+  σ !! l = Some v' → v' ≠ v1 →
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitBool false))
-  ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
-    ?right_id //; last (by intros; inv_head_step; eauto);
-    simpl; by eauto 10.
+  intros ??.
+  rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
+    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
-Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
+Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
+  σ !! l = Some v1 →
   ▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) ={E}=★ Φ (LitV $ LitBool true))
-  ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
-    (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto);
-    simpl; by eauto 10.
+  intros ?. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
+    (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto).
+  solve_atomic.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 6ac1972a7f27d3559d905ab89d8c9c15dc6a941d..da060db51554e3dd23928e7676e1ddd7cda84891 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -183,10 +183,20 @@ Definition atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma atomic_correct e : atomic e → heap_lang.atomic (to_expr e).
+Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
 Proof.
-  destruct e; simpl; repeat (case_match; try done);
-    naive_solver eauto using to_val_is_Some.
+  intros He. apply ectx_language_atomic.
+  - intros σ e' σ' ef.
+    destruct e; simpl; try done; repeat (case_match; try done);
+    inversion 1; rewrite ?to_of_val; eauto. subst.
+    unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
+  - intros [|Ki K] e' Hfill Hnotval; [done|exfalso].
+    apply (fill_not_val K), eq_None_not_Some in Hnotval. apply Hnotval. simpl.
+    revert He. destruct e; simpl; try done; repeat (case_match; try done);
+    rewrite ?bool_decide_spec;
+    destruct Ki; inversion Hfill; subst; clear Hfill;
+    try naive_solver eauto using to_val_is_Some.
+    move=> _ /=; destruct decide as [|Nclosed]; [by eauto | by destruct Nclosed].
 Qed.
 End W.
 
@@ -213,16 +223,11 @@ Ltac solve_to_val :=
   end.
 
 Ltac solve_atomic :=
-  try match goal with
-  | |- context E [language.atomic ?e] =>
-     let X := context E [atomic e] in change X
-  end;
   match goal with
-  | |- atomic ?e =>
-     let e' := W.of_expr e in change (atomic (W.to_expr e'));
+  | |- language.atomic ?e =>
+     let e' := W.of_expr e in change (language.atomic (W.to_expr e'));
      apply W.atomic_correct; vm_compute; exact I
   end.
-Hint Extern 0 (atomic _) => solve_atomic : fsaV.
 Hint Extern 0 (language.atomic _) => solve_atomic : fsaV.
 
 (** Substitution *)
diff --git a/prelude/base.v b/prelude/base.v
index 86b1036fb2c416eb10b7c9f30377b42f52db988c..f354f0e0b635da187966d0fd8320d8e178d9a2e9 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -590,7 +590,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope.
 
 Class Difference A := difference: A → A → A.
 Instance: Params (@difference) 2.
-Infix "∖" := difference (at level 40) : C_scope.
+Infix "∖" := difference (at level 40, left associativity) : C_scope.
 Notation "(∖)" := difference (only parsing) : C_scope.
 Notation "( x ∖)" := (difference x) (only parsing) : C_scope.
 Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope.
diff --git a/program_logic/ectx_language.v b/program_logic/ectx_language.v
index 161f41ea446a42e96187bababf8492d2fe544aeb..d7b58df92eac2bd6fbc9ce115420f19454bfd68b 100644
--- a/program_logic/ectx_language.v
+++ b/program_logic/ectx_language.v
@@ -11,7 +11,6 @@ Class EctxLanguage (expr val ectx state : Type) := {
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  atomic : expr → Prop;
   head_step : expr → state → expr → state → option expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
@@ -34,16 +33,6 @@ Class EctxLanguage (expr val ectx state : Type) := {
     to_val e1 = None →
     head_step e1' σ1 e2 σ2 ef →
     exists K'', K' = comp_ectx K K'';
-
-  atomic_not_val e : atomic e → to_val e = None;
-  atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 →
-    head_step e1 σ1 e2 σ2 ef →
-    is_Some (to_val e2);
-  atomic_fill e K :
-    atomic (fill K e) →
-    to_val e = None →
-    K = empty_ectx;
 }.
 
 Arguments of_val {_ _ _ _ _} _.
@@ -51,7 +40,6 @@ Arguments to_val {_ _ _ _ _} _.
 Arguments empty_ectx {_ _ _ _ _}.
 Arguments comp_ectx {_ _ _ _ _} _ _.
 Arguments fill {_ _ _ _ _} _ _.
-Arguments atomic {_ _ _ _ _} _.
 Arguments head_step {_ _ _ _ _} _ _ _ _ _.
 
 Arguments to_of_val {_ _ _ _ _} _.
@@ -62,9 +50,6 @@ Arguments fill_comp {_ _ _ _ _} _ _ _.
 Arguments fill_not_val {_ _ _ _ _} _ _ _.
 Arguments ectx_positive {_ _ _ _ _} _ _ _.
 Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
-Arguments atomic_not_val {_ _ _ _ _} _ _.
-Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments atomic_fill {_ _ _ _ _} _ _ _ _.
 
 (* From an ectx_language, we can construct a language. *)
 Section ectx_language.
@@ -84,23 +69,12 @@ Section ectx_language.
     prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
   Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.
 
-  Lemma atomic_prim_step e1 σ1 e2 σ2 ef :
-    atomic e1 → prim_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
-  Proof.
-    intros Hatomic [K e1' e2' -> -> Hstep].
-    assert (K = empty_ectx) as -> by eauto 10 using atomic_fill, val_stuck.
-    revert Hatomic; rewrite !fill_empty. eauto using atomic_step.
-  Qed.
-
   Canonical Structure ectx_lang : language := {|
     language.expr := expr; language.val := val; language.state := state;
     language.of_val := of_val; language.to_val := to_val;
-    language.atomic := atomic;
     language.prim_step := prim_step;
     language.to_of_val := to_of_val; language.of_to_val := of_to_val;
     language.val_stuck := val_prim_stuck;
-    language.atomic_not_val := atomic_not_val;
-    language.atomic_step := atomic_prim_step
   |}.
 
   (* Some lemmas about this language *)
@@ -111,6 +85,16 @@ Section ectx_language.
   Lemma head_prim_reducible e σ : head_reducible e σ → reducible e σ.
   Proof. intros (e'&σ'&ef&?). eexists e', σ', ef. by apply head_prim_step. Qed.
 
+  Lemma ectx_language_atomic e :
+    (∀ σ e' σ' ef, head_step e σ e' σ' ef → is_Some (to_val e')) →
+    (∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx) →
+    atomic e.
+  Proof.
+    intros Hatomic_step Hatomic_fill σ e' σ' ef [K e1' e2' -> -> Hstep].
+    assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
+    rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
+  Qed.
+
   Lemma head_reducible_prim_step e1 σ1 e2 σ2 ef :
     head_reducible e1 σ1 → prim_step e1 σ1 e2 σ2 ef →
     head_step e1 σ1 e2 σ2 ef.
diff --git a/program_logic/ectxi_language.v b/program_logic/ectxi_language.v
index b09713b0e370c84dd3616136ca445da04e69dc50..4a8f62fd85863f80c4946907b42602a29e98fc3d 100644
--- a/program_logic/ectxi_language.v
+++ b/program_logic/ectxi_language.v
@@ -9,7 +9,6 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
   of_val : val → expr;
   to_val : expr → option val;
   fill_item : ectx_item → expr → expr;
-  atomic : expr → Prop;
   head_step : expr → state → expr → state → option expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
@@ -24,20 +23,11 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
 
   head_ctx_step_val Ki e σ1 e2 σ2 ef :
     head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e);
-
-  atomic_not_val e : atomic e → to_val e = None;
-  atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 →
-    head_step e1 σ1 e2 σ2 ef →
-    is_Some (to_val e2);
-  atomic_fill_item e Ki :
-    atomic (fill_item Ki e) → is_Some (to_val e)
 }.
 
 Arguments of_val {_ _ _ _ _} _.
 Arguments to_val {_ _ _ _ _} _.
 Arguments fill_item {_ _ _ _ _} _ _.
-Arguments atomic {_ _ _ _ _} _.
 Arguments head_step {_ _ _ _ _} _ _ _ _ _.
 
 Arguments to_of_val {_ _ _ _ _} _.
@@ -47,9 +37,6 @@ Arguments fill_item_val {_ _ _ _ _} _ _ _.
 Arguments fill_item_no_val_inj {_ _ _ _ _} _ _ _ _ _ _ _.
 Arguments head_ctx_step_val {_ _ _ _ _} _ _ _ _ _ _ _.
 Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
-Arguments atomic_not_val {_ _ _ _ _} _ _.
-Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments atomic_fill_item {_ _ _ _ _} _ _ _.
 
 Section ectxi_language.
   Context {expr val ectx_item state}
@@ -70,12 +57,6 @@ Section ectxi_language.
   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 atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
-  Proof.
-    destruct K as [|Ki K]; [done|].
-    rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
-  Qed.
-
   (* 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 *)
@@ -95,10 +76,9 @@ Section ectxi_language.
   Global Program Instance : EctxLanguage expr val ectx state :=
     (* For some reason, Coq always rejects the record syntax claiming I
        fixed fields of different records, even when I did not. *)
-    Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill atomic head_step _ _ _ _ _ _ _ _ _ _ _ _.
+    Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill head_step _ _ _ _ _ _ _ _ _.
   Solve Obligations with eauto using to_of_val, of_to_val, val_stuck,
-    atomic_not_val, atomic_step, fill_not_val, atomic_fill,
-    step_by_val, fold_right_app, app_eq_nil.
+    fill_not_val, step_by_val, fold_right_app, app_eq_nil.
 
   Global Instance ectxi_lang_ctx_item Ki :
     LanguageCtx (ectx_lang expr) (fill_item Ki).
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 25623bb115fe020db8e88ccd1cb7d163b1990f58..1654324b6094bcccb26876512e9308e318505541 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -49,12 +49,12 @@ Proof.
   iApply (ht_lift_step E E _ (λ σ1', P ∧ σ1 = σ1')%I
            (λ e2 σ2 ef, ownP σ2 ★ ■ (is_Some (to_val e2) ∧ prim_step e1 σ1 e2 σ2 ef))%I
            (λ e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ P)%I);
-    try by (eauto using atomic_not_val).
+    try by (eauto using reducible_not_val).
   repeat iSplit.
   - iIntros "![Hσ1 HP]". iExists σ1. iPvsIntro.
-    iSplit. by eauto using atomic_step. iFrame. by auto.
+    iSplit. by eauto. iFrame. by auto.
   - iIntros (? e2 σ2 ef) "! (%&Hown&HP&%)". iPvsIntro. subst.
-    iFrame. iSplit; iPureIntro; auto. split; eauto using atomic_step.
+    iFrame. iSplit; iPureIntro; auto. split; eauto.
   - iIntros (e2 σ2 ef) "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
     iApply wp_value'. iExists σ2, ef. by iSplit.
   - done.
diff --git a/program_logic/language.v b/program_logic/language.v
index fb97505aaa82fb3fd947357982b2ac30261dcea8..33600f6dfce705774c1a66d601f6bfcb7c46e4ae 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -6,26 +6,17 @@ Structure language := Language {
   state : Type;
   of_val : val → expr;
   to_val : expr → option val;
-  atomic : expr → Prop;
   prim_step : expr → state → expr → state → option expr → Prop;
   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;
-  val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → 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 →
-    is_Some (to_val e2)
+  val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None
 }.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
-Arguments atomic {_} _.
 Arguments prim_step {_} _ _ _ _ _.
 Arguments to_of_val {_} _.
 Arguments of_to_val {_} _ _ _.
 Arguments val_stuck {_} _ _ _ _ _ _.
-Arguments atomic_not_val {_} _ _.
-Arguments atomic_step {_} _ _ _ _ _ _ _.
 
 Canonical Structure stateC Λ := leibnizC (state Λ).
 Canonical Structure valC Λ := leibnizC (val Λ).
@@ -39,6 +30,8 @@ Section language.
 
   Definition reducible (e : expr Λ) (σ : state Λ) :=
     ∃ e' σ' ef, prim_step e σ e' σ' ef.
+  Definition atomic (e : expr Λ) : Prop :=
+    ∀ σ e' σ' ef, prim_step e σ e' σ' ef → is_Some (to_val e').
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
@@ -50,8 +43,6 @@ Section language.
   Proof. intros <-. by rewrite to_of_val. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
-  Lemma atomic_of_val v : ¬atomic (of_val v).
-  Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed.
   Global Instance: Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 End language.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 0de2b8be7b7c17744968cb29710f0bca6dbfd6a0..6b98cf087a3aea1de5f51eb74755aa4bd9e2e7f3 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -67,10 +67,10 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
     ■ prim_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (??) "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); auto using atomic_not_val.
-  iPvsIntro. iExists σ1. repeat iSplit; eauto 10 using atomic_step.
+  iIntros (Hatom ?) "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); eauto using reducible_not_val.
+  iPvsIntro. iExists σ1. repeat iSplit; eauto 10.
   iFrame. iNext. iIntros (e2 σ2 ef) "[% Hσ2]".
-  edestruct @atomic_step as [v2 Hv%of_to_val]; eauto. subst e2.
+  edestruct Hatom as [v2 Hv%of_to_val]; eauto. subst e2.
   iDestruct ("Hwp" $! v2 σ2 ef with "[Hσ2]") as "[HΦ ?]". by eauto.
   iFrame. iPvs "HΦ". iPvsIntro. iApply wp_value; auto using to_of_val.
 Qed.
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 9950d42d348fca40966192e47bb7e541040920d4..ee59788b16cd3cbfff5a1fd16605e836d93c46c2 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -77,7 +77,7 @@ Section ndisjoint.
 End ndisjoint.
 
 (* The hope is that registering these will suffice to solve most goals
-of the form [N1 ⊥ N2] and those of the form [((N1 ⊆ E ∖ N2) ∖ ..) ∖ Nn]. *)
+of the form [N1 ⊥ N2] and those of the form [N1 ⊆ E ∖ N2 ∖ .. ∖ Nn]. *)
 Hint Resolve ndisj_subseteq_difference : ndisj.
 Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l : ndisj.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index c87539c436ddf75373b4c9501ea3c72c7f1a78b1..ab2d859b938a2cc26388a2422e7a5036c588c36a 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -160,20 +160,25 @@ Lemma wp_atomic E1 E2 e Φ :
   E2 ⊆ E1 → atomic e →
   (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
 Proof.
-  rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs; constructor.
-  eauto using atomic_not_val. intros k Ef σ1 rf ???.
-  destruct (Hvs (S k) Ef σ1 rf) as (r'&Hwp&?); auto.
-  destruct (wp_step_inv E2 Ef (pvs_def E2 E1 ∘ Φ) e k (S k) σ1 r' rf)
-    as [Hsafe Hstep]; auto using atomic_not_val; [].
-  split; [done|]=> e2 σ2 ef ?.
-  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
-  destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
-    [|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver].
-  rewrite -pvs_eq in Hvs'. apply pvs_trans in Hvs';auto. rewrite pvs_eq in Hvs'.
-  destruct (Hvs' k Ef σ2 (r2' ⋅ rf)) as (r3&[]); rewrite ?assoc; auto.
-  exists r3, r2'; split_and?; last done.
-  - by rewrite -assoc.
-  - constructor; apply pvs_intro; auto.
+  rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs.
+  destruct (Some_dec (to_val e)) as [[v <-%of_to_val]|].
+  - eapply wp_pre_value. rewrite pvs_eq.
+    intros k Ef σ rf ???. destruct (Hvs k Ef σ rf) as (r'&Hwp&?); auto.
+    apply wp_value_inv in Hwp. rewrite pvs_eq in Hwp.
+    destruct (Hwp k Ef σ rf) as (r2'&HΦ&?); auto.
+  - apply wp_pre_step. done. intros k Ef σ1 rf ???.
+    destruct (Hvs (S k) Ef σ1 rf) as (r'&Hwp&?); auto.
+    destruct (wp_step_inv E2 Ef (pvs_def E2 E1 ∘ Φ) e k (S k) σ1 r' rf)
+      as [Hsafe Hstep]; auto; [].
+    split; [done|]=> e2 σ2 ef ?.
+    destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
+    destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
+      [|destruct (He σ1 e2 σ2 ef); naive_solver].
+    rewrite -pvs_eq in Hvs'. apply pvs_trans in Hvs';auto. rewrite pvs_eq in Hvs'.
+    destruct (Hvs' k Ef σ2 (r2' ⋅ rf)) as (r3&[]); rewrite ?assoc; auto.
+    exists r3, r2'; split_and?; last done.
+    + by rewrite -assoc.
+    + constructor; apply pvs_intro; auto.
 Qed.
 Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }} ★ R ⊢ WP e @ E {{ v, Φ v ★ R }}.
 Proof.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 650238ddd5f910f70db52d1ad6c6e925b097d6a4..0392bd540d540693f8d5f132c8faa2e6afe28f3b 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -51,17 +51,17 @@ Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r.
 Proof.
   destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).
   intros [rs [Hval Hσ HE Hwld]] ?; exists rs; constructor; auto.
-  intros i P ? HiP; destruct (wld (r â‹… big_opM rs) !! i) as [P'|] eqn:HP';
-    [apply (inj Some) in HiP|inversion_clear HiP].
+  intros i P ? (P'&HiP&HP')%dist_Some_inv_r'.
+  destruct (to_agree_uninj (S n) P') as [laterP' HlaterP'].
+  { apply (lookup_validN_Some _ (wld (r â‹… big_opM rs)) i); rewrite ?HiP; auto. }
   assert (P' ≡{S n}≡ to_agree $ Next $ iProp_unfold $
-                       iProp_fold $ later_car $ P' (S n)) as HPiso.
-  { rewrite iProp_unfold_fold later_eta to_agree_car //.
-    apply (lookup_validN_Some _ (wld (r â‹… big_opM rs)) i); rewrite ?HP'; auto. }
-  assert (P ≡{n'}≡ iProp_fold (later_car (P' (S n)))) as HPP'.
+                       iProp_fold $ later_car $ laterP') as HPiso.
+  { by rewrite iProp_unfold_fold later_eta HlaterP'. }
+  assert (P ≡{n'}≡ iProp_fold (later_car laterP')) as HPP'.
   { apply (inj iProp_unfold), (inj Next), (inj to_agree).
-    by rewrite -HiP -(dist_le _ _ _ _ HPiso). }
-  destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto.
-  { by rewrite HP' -HPiso. }
+    by rewrite HP' -(dist_le _ _ _ _ HPiso). }
+  destruct (Hwld i (iProp_fold (later_car laterP'))) as (r'&?&?); auto.
+  { by rewrite HiP -HPiso. }
   assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto).
   exists r'; split; [done|]. apply HPP', uPred_closed with n; auto.
 Qed.