diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index c0246453727e3d9baa9a73febe08a74cdbabce44..942c1aa93ebedde7266e52785607866515f6f2b5 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -68,11 +68,6 @@
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
-"not_cas_compare_safe"
-     : string
-The command has indeed failed with message:
-Ltac call to "wp_cas_suc" failed.
-Tactic failure: wp_cas_suc: Values are not safe to compare for CAS.
 "not_cas"
      : string
 The command has indeed failed with message:
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 54d46b46ef9bc01636f03c15603096acb829056e..0d93617243d23e00a0f86e06747292644b30a9e3 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -116,6 +116,13 @@ Section tests.
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
 
+  Lemma wp_cas l v :
+    val_is_unboxed v →
+    l ↦ v -∗ WP CAS #l v v {{ _, True }}.
+  Proof.
+    iIntros (?) "?". wp_cas as ? | ?. done. done.
+  Qed.
+
 End tests.
 
 Section printing_tests.
@@ -166,13 +173,6 @@ End printing_tests.
 Section error_tests.
   Context `{heapG Σ}.
 
-  Check "not_cas_compare_safe".
-  Lemma not_cas_compare_safe (l : loc) (v : val) :
-    l ↦ v -∗ WP CAS #l v v {{ _, True }}.
-  Proof.
-    iIntros "H↦". Fail wp_cas_suc.
-  Abort.
-
   Check "not_cas".
   Lemma not_cas :
     (WP #() {{ _, True }})%I.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 30eb83c697b0b4b27ef576356895d4b2c908c073..322bd54490fe69f05a26db3ee7e94a300992c254 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -68,9 +68,6 @@ Inductive expr :=
 
 Bind Scope expr_scope with expr.
 
-Notation NONE := (InjL (Lit LitUnit)) (only parsing).
-Notation SOME x := (InjR x) (only parsing).
-
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
   | Var x => bool_decide (x ∈ X)
@@ -99,9 +96,6 @@ Inductive val :=
 
 Bind Scope val_scope with val.
 
-Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
-Notation SOMEV x := (InjRV x) (only parsing).
-
 Fixpoint of_val (v : val) : expr :=
   match v with
   | RecV f x e => Rec f x e
@@ -122,6 +116,38 @@ Fixpoint to_val (e : expr) : option val :=
   | _ => None
   end.
 
+(** We assume the following encoding of values to 64-bit words: The least 3
+significant bits of every word are a "tag", and we have 61 bits of payload,
+which is enough if all pointers are 8-byte-aligned (common on 64bit
+architectures). The tags have the following meaning:
+
+0: Payload is the data for a LitV (LitInt _).
+1: Payload is the data for a InjLV (LitV (LitInt _)).
+2: Payload is the data for a InjRV (LitV (LitInt _)).
+3: Payload is the data for a LitV (LitLoc _).
+4: Payload is the data for a InjLV (LitV (LitLoc _)).
+4: Payload is the data for a InjRV (LitV (LitLoc _)).
+6: Payload is one of the following finitely many values, which 61 bits are more
+   than enough to encode:
+   LitV LitUnit, InjLV (LitV LitUnit), InjRV (LitV LitUnit),
+   LitV (LitBool _), InjLV (LitV (LitBool _)), InjRV (LitV (LitBool _)).
+7: Value is boxed, i.e., payload is a pointer to some read-only memory area on
+   the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
+   relevant data for those cases. However, the boxed representation is never
+   used if any of the above representations could be used.
+
+Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
+bits, this means every value is machine-word-sized and can hence be atomically
+read and written.  Also notice that the sets of boxed and unboxed values are
+disjoint. *)
+Definition val_is_unboxed (v : val) : Prop :=
+  match v with
+  | LitV _ => True
+  | InjLV (LitV _) => True
+  | InjRV (LitV _) => True
+  | _ => False
+  end.
+
 (** The state: heaps of vals. *)
 Definition state := gmap loc val.
 
@@ -367,53 +393,13 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
   | _, _ => None
   end.
 
-(** Return whether it is possible to use CAS to compare vl (current value) with
-v1 (netest value).
-
-We assume the following encoding of values to 64-bit words: The least 3
-significant bits of every word are a "tag", and we have 61 bits of payload,
-which is enough if all pointers are 8-byte-aligned (commong on 64bit
-architectures). The tags have the following meaning:
-
-0: Payload is one of the following finitely many values, which 61 bits are more
-   than enough to encode: LitV LitUnit, LitV (LitBool _), NONEV, SOMEV (LitV
-   LitUnit), SOMEV (LitV (LitBool _)).
-1: Payload is the data for a LitV (LitInt _).
-2: Payload is the data for a SOMEV (LitV (LitInt _)).
-3: Payload is the data for a LitV (LitLoc _).
-4: Payload is the data for a SOMEV (LitV (LitLoc _)).
-5: Value is boxed, i.e., payload is a pointer to some read-only memory area on
-   the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
-   relevant data for those cases. However, the boxed representation is never
-   used if any of the above representations could be used.
-6: Unused.
-7: Unused.
-
-Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
-bits, this means every value is machine-word-sized and can hence be atomically
-read and written. It also justifies the comparisons allowed for CAS: Whenever
-[vals_cas_compare_safe vl v1] holds, equality of the one-word representation of
-[vl] and [v1] is equivalent to equality of the abstract value represented. This
-is clear for [LitV _ == LitV _] and [SOMEV (LitV _) == SOMEV (LitV _)] because
-none of these are boxed. For [NONEV == v], we can't actually atomically load and
-compare the data for boxed values, but that's okay because we only have to know
-if they are equal to [NONEV] which is distinct from all boxed values.
- *)
+(** CAS just compares the word-sized representation of the two values, it cannot
+look into boxed data.  This works out fine if at least one of the to-be-compared
+values is unboxed (exploiting the fact that an unboxed and a boxed value can
+never be equal because these are disjoint sets).  *)
 Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
-  match vl, v1 with
-  (* We allow comparing literals with each other, also when wrapped in a SOMEV. *)
-  | LitV _, LitV _ => True
-  | SOMEV (LitV _), SOMEV (LitV _) => True
-  (* We allow comparing NONEV to anything. *)
-  | NONEV, _ => True
-  | _, NONEV => True
-  (* We don't allow comparing anything else. *)
-  | _, _ => False
-  end.
-(** Just a sanity check. *)
-Lemma vals_cas_compare_safe_sym vl v1 :
-  vals_cas_compare_safe vl v1 → vals_cas_compare_safe v1 vl.
-Proof. rewrite /vals_cas_compare_safe. repeat case_match; done. Qed.
+  val_is_unboxed vl ∨ val_is_unboxed v1.
+Arguments vals_cas_compare_safe !_ !_ /.
 
 Inductive head_step : expr → state → expr → state → list (expr) → Prop :=
   | BetaS f x e1 e2 v2 e' σ :
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index 9de110430c2391ff9789cd62b8731dd50c72a9c0..ad3f079a38ab3281c597ca7b9ed075d1ccbbcd12 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -33,11 +33,15 @@ Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
               (λ v, mapsto l 1 v)
               (λ v (_:()), mapsto l 1 w)
               (λ _ _, #()%V);
+  (* This spec is slightly weaker than it could be: It is sufficient for [w1]
+  *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
+  is outside the atomic triple, which makes it much easier to use -- and the
+  spec is still good enough for all our applications. *)
   cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
-    IntoVal e1 w1 → IntoVal e2 w2 →
+    IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
     atomic_wp (cas (#l, e1, e2))%E
               ⊤ ⊤
-              (λ v, ⌜vals_cas_compare_safe v w1⌝ ∗ mapsto l 1 v)%I
+              (λ v, mapsto l 1 v)%I
               (λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v)
               (λ v _, #(if decide (v = w1) then true else false)%V);
 }.
@@ -88,16 +92,16 @@ Section proof.
   Qed.
 
   Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
-    IntoVal e1 w1 → IntoVal e2 w2 →
+    IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
     atomic_wp (primitive_cas (#l, e1, e2))%E
               ⊤ ⊤
-              (λ v, ⌜vals_cas_compare_safe v w1⌝ ∗ l ↦ v)%I
+              (λ v, l ↦ v)%I
               (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I
               (λ v _, #(if decide (v = w1) then true else false)%V).
   Proof.
-    iIntros (<- <- Q Φ) "? AU". wp_let. repeat wp_proj.
-    iMod (aupd_acc with "AU") as (v) "[[% H↦] [_ Hclose]]"; first solve_ndisj.
-    destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail];
+    iIntros (<- <- ? Q Φ) "? AU". wp_let. repeat wp_proj.
+    iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
+    destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
     iMod ("Hclose" $! () with "H↦") as "HΦ"; by iApply "HΦ".
   Qed.
 
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index d2db12190118428c6ce2cdb6dde671a1b563086f..4640f7c0167214e2bc091b1c408e6280dae655ae 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -35,12 +35,12 @@ Section increment.
     iIntros ([]) "$ !> AU !> HQ".
     (* Now go on *)
     wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
-    wp_apply (cas_spec with "[HQ]"); first by iAccu.
+    wp_apply (cas_spec with "[HQ]"); first done; first by iAccu.
     (* Prove the atomic shift for CAS *)
     iAuIntro. iApply (aacc_aupd with "AU"); first done.
     iIntros (x') "H↦".
-    iApply (aacc_intro with "[H↦]"); [solve_ndisj|simpl;by auto with iFrame|iSplit].
-    { iIntros "[_ $] !> $ !> //". }
+    iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
+    { eauto 10 with iFrame. }
     iIntros ([]) "H↦ !>".
     destruct (decide (#x' = #x)) as [[= ->]|Hx].
     - iRight. iExists (). iFrame. iIntros "HΦ !> HQ".
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index d991e108db625e970de4409058fc7f4ea3f67786..f8ef7a58517e001c25d35b3bcbeccdcbc9714547 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -144,6 +144,12 @@ Notation "e1 || e2" :=
   (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
 
 (** Notations for option *)
+Notation NONE := (InjL (Lit LitUnit)) (only parsing).
+Notation SOME x := (InjR x) (only parsing).
+
+Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
+Notation SOMEV x := (InjRV x) (only parsing).
+
 Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 17236f403ce7ba382d87045b2efb29ba50c42e59..58b7feee3a272384df955d67546f7f7ce47e4d16 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -221,10 +221,49 @@ Proof.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
 
+Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
+  vals_cas_compare_safe v v1 →
+  (v = v1 → envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }})) →
+  (v ≠ v1 → envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq=> ?????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
+  - rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
+    rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
+    apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
+  - rewrite -wp_bind. eapply wand_apply.
+    { eapply wp_cas_fail; eauto. by eexists. }
+    rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
+    apply later_mono, sep_mono_r. apply wand_mono; auto.
+Qed.
+Lemma tac_twp_cas Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  envs_lookup i Δ = Some (false, l ↦ v)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
+  vals_cas_compare_safe v v1 →
+  (v = v1 → envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }])) →
+  (v ≠ v1 → envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
+Proof.
+  rewrite envs_entails_eq=> ????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
+  - rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
+    rewrite /= {1}envs_simple_replace_sound //; simpl.
+    apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
+  - rewrite -twp_bind. eapply wand_apply.
+    { eapply twp_cas_fail; eauto. by eexists. }
+    rewrite /= {1}envs_lookup_split //; simpl.
+    apply sep_mono_r. apply wand_mono; auto.
+Qed.
+
 Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 → vals_cas_compare_safe v v1 →
+  envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
+  v ≠ v1 → vals_cas_compare_safe v v1 →
   envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
@@ -235,7 +274,8 @@ Proof.
 Qed.
 Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
-  envs_lookup i Δ = Some (false, l ↦{q} v)%I → v ≠ v1 → vals_cas_compare_safe v v1 →
+  envs_lookup i Δ = Some (false, l ↦{q} v)%I →
+  v ≠ v1 → vals_cas_compare_safe v v1 →
   envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
 Proof.
@@ -247,25 +287,29 @@ Qed.
 Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 → vals_cas_compare_safe v v1 →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
+  v = v1 → val_is_unboxed v →
   envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ????????; subst.
-  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
+  rewrite -wp_bind. eapply wand_apply.
+  { eapply wp_cas_suc; eauto. by left. }
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 Lemma tac_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
-  envs_lookup i Δ = Some (false, l ↦ v)%I → v = v1 → vals_cas_compare_safe v v1 →
+  envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
+  v = v1 → val_is_unboxed v →
   envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq. intros; subst.
-  rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
+  rewrite -twp_bind. eapply wand_apply.
+  { eapply twp_cas_suc; eauto. by left. }
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
@@ -392,6 +436,36 @@ Tactic Notation "wp_store" :=
   | _ => fail "wp_store: not a 'wp'"
   end.
 
+Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_cas: cannot find" l "↦ ?" in
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_wp_cas _ _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
+      |fail 1 "wp_cas: cannot find 'CAS' in" e];
+    [iSolveTC
+    |solve_mapsto ()
+    |pm_reflexivity
+    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
+    |intros H1; wp_expr_simpl; try wp_value_head
+    |intros H2; wp_expr_simpl; try wp_value_head]
+  | |- envs_entails _ (twp ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_cas _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
+      |fail 1 "wp_cas: cannot find 'CAS' in" e];
+    [solve_mapsto ()
+    |pm_reflexivity
+    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
+    |intros H1; wp_expr_simpl; try wp_value_head
+    |intros H2; wp_expr_simpl; try wp_value_head]
+  | _ => fail "wp_cas: not a 'wp'"
+  end.
+
 Tactic Notation "wp_cas_fail" :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
@@ -406,7 +480,7 @@ Tactic Notation "wp_cas_fail" :=
     [iSolveTC
     |solve_mapsto ()
     |try congruence
-    |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
+    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
@@ -415,7 +489,7 @@ Tactic Notation "wp_cas_fail" :=
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
-    |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
+    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_fail: not a 'wp'"
   end.
@@ -433,9 +507,9 @@ Tactic Notation "wp_cas_suc" :=
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [iSolveTC
     |solve_mapsto ()
-    |try congruence
-    |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
     |pm_reflexivity
+    |try congruence
+    |try fast_done (* vals_cas_compare_safe *)
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
     first
@@ -443,9 +517,9 @@ Tactic Notation "wp_cas_suc" :=
          eapply (tac_twp_cas_suc _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [solve_mapsto ()
-    |try congruence
-    |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
     |pm_reflexivity
+    |try congruence
+    |try fast_done (* vals_cas_compare_safe *)
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_suc: not a 'wp'"
   end.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 20abcb4fc6d5550a654e2a3e82e5cbbd26898e53..2ccfba251032b1299db668b16ec3bcbbefce27d9 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -65,18 +65,27 @@ Proof. apply envs_lookup_sound'. Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
   envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ.
 Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
+Lemma envs_lookup_sound_2 Δ i p P :
+  envs_wf Δ → envs_lookup i Δ = Some (p,P) →
+  □?p P ∗ of_envs (envs_delete true i p Δ) ⊢ of_envs Δ.
+Proof.
+  rewrite /envs_lookup /of_envs=>Hwf ?. rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
+  - rewrite (env_lookup_perm Γp) //= intuitionistically_and
+      and_sep_intuitionistically and_elim_r.
+    cancel [â–¡ P]%I. solve_sep_entails.
+  - destruct (Γs !! i) eqn:?; simplify_eq/=.
+    rewrite (env_lookup_perm Γs) //= and_elim_r.
+    cancel [P]. solve_sep_entails.
+Qed.
 
 Lemma envs_lookup_split Δ i p P :
   envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ (□?p P -∗ of_envs Δ).
 Proof.
-  rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
-  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
-  - rewrite pure_True // left_id (env_lookup_perm Γp) //=
-      intuitionistically_and and_sep_intuitionistically.
-    cancel [â–¡ P]%I. apply wand_intro_l. solve_sep_entails.
-  - destruct (Γs !! i) eqn:?; simplify_eq/=.
-    rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
-    cancel [P]. apply wand_intro_l. solve_sep_entails.
+  intros. apply pure_elim with (envs_wf Δ).
+  { rewrite of_envs_eq. apply and_elim_l. }
+  intros. rewrite {1}envs_lookup_sound//.
+  apply sep_mono_r. apply wand_intro_l, envs_lookup_sound_2; done.
 Qed.
 
 Lemma envs_lookup_delete_sound Δ Δ' rp i p P :
@@ -198,6 +207,17 @@ Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   of_envs Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
+Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
+  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
+  of_envs Δ ⊢ □?p P ∗ (((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)).
+Proof.
+  intros. apply pure_elim with (envs_wf Δ).
+  { rewrite of_envs_eq. apply and_elim_l. }
+  intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r, and_intro.
+  - rewrite envs_simple_replace_sound'//.
+  - apply wand_intro_l, envs_lookup_sound_2; done.
+Qed.
+
 Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
   envs_lookup i Δ = Some (p,P) →
   envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →