diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 6061d0eb65a88f0d67eda52f20055180793e2d66..2251d52c218f87e4a0ed183c71014a12cf4c189f 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -47,7 +47,7 @@ Ltac inv_head_step :=
      inversion H; subst; clear H
   end.
 
-Local Hint Extern 0 (strongly_atomic _) => solve_atomic.
+Local Hint Extern 0 (atomic _ _) => solve_atomic.
 Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
 
 Local Hint Constructors head_step.
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 201e3cad7a2d95aed1de8f6f0a08d449df3524eb..fd3fcd6354eb251b61d33dab429f74ce51af388e 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -187,9 +187,11 @@ Definition is_atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma is_atomic_correct e : is_atomic e → StronglyAtomic (to_expr e).
+Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
 Proof.
-  intros He. apply ectx_language_strong_atomic.
+  enough (is_atomic e → Atomic maybe_stuck (to_expr e)).
+  { destruct s; auto using strongly_atomic_atomic. }
+  intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
     destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
@@ -226,15 +228,11 @@ Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
-  | |- StronglyAtomic ?e =>
-     let e' := W.of_expr e in change (StronglyAtomic (W.to_expr e'));
+  | |- Atomic ?s ?e =>
+     let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
      apply W.is_atomic_correct; vm_compute; exact I
-  | |- Atomic ?e =>
-     let e' := W.of_expr e in change (Atomic (W.to_expr e'));
-     apply strongly_atomic_atomic, W.is_atomic_correct; vm_compute; exact I
   end.
-Hint Extern 10 (StronglyAtomic _) => solve_atomic : typeclass_instances.
-Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
+Hint Extern 10 (Atomic _ _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 642f715426d8c4dd3ec2788b90113d09f8afc4f8..8d7dbf1eeb15478fa570d905eb60019041a804c2 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -91,6 +91,11 @@ Section ectx_language.
     language.val_stuck := val_prim_stuck;
   |}.
 
+  Class HeadAtomic (s : stuckness) (e : expr) : Prop :=
+    head_atomic σ e' σ' efs :
+      head_step e σ e' σ' efs →
+      if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
+
   (* Some lemmas about this language *)
   Lemma head_prim_step e1 σ1 e2 σ2 efs :
     head_step e1 σ1 e2 σ2 efs → prim_step e1 σ1 e2 σ2 efs.
@@ -127,20 +132,8 @@ Section ectx_language.
     exists K, e1'. split; first done. by exists e2', σ', efs.
   Qed.
 
-  Lemma ectx_language_strong_atomic e :
-    (∀ σ e' σ' efs, head_step e σ e' σ' efs → is_Some (to_val e')) →
-    sub_redexes_are_values e →
-    StronglyAtomic e.
-  Proof.
-    intros Hatomic_step Hatomic_fill σ e' σ' efs [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 ectx_language_atomic e :
-    (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
-    sub_redexes_are_values e →
-    Atomic e.
+  Lemma ectx_language_atomic s e :
+    HeadAtomic s e → sub_redexes_are_values e → Atomic s e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 549db62c565dcf36658a84f1caf4ee943c56f5ff..44d6aed64f27def546f4beb6f625d81d15577daa 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -76,29 +76,16 @@ Proof.
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_atomic' s E1 E2 P P' Φ Φ' e :
-  StronglyAtomic e ∨ s = not_stuck ∧ Atomic e →
+Lemma ht_atomic s E1 E2 P P' Φ Φ' e `{!Atomic s e} :
   (P ={E1,E2}=> P') ∧ {{ P' }} e @ s; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ s; E1 {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic' _ _ E2); auto.
+  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
   iMod ("Hvs" with "HP") as "HP". iModIntro.
   iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_strong_atomic s E1 E2 P P' Φ Φ' e :
-  StronglyAtomic e →
-  (P ={E1,E2}=> P') ∧ {{ P' }} e @ s; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
-  ⊢ {{ P }} e @ s; E1 {{ Φ }}.
-Proof. by eauto using ht_atomic'. Qed.
-
-Lemma ht_atomic E1 E2 P P' Φ Φ' e :
-  Atomic e →
-  (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
-  ⊢ {{ P }} e @ E1 {{ Φ }}.
-Proof. by eauto using ht_atomic'. Qed.
-
 Lemma ht_bind `{LanguageCtx Λ K} s E P Φ Φ' e :
   {{ P }} e @ s; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
   ⊢ {{ P }} K e @ s; E {{ Φ' }}.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 0bf6c5ee6e2d26d93691811bd8c3cbb505e7c04c..6d96db0b1f4f04b00c9ac9b2861c6751b889ae8f 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -56,21 +56,21 @@ Section language.
   Definition progressive (e : expr Λ) (σ : state Λ) :=
     is_Some (to_val e) ∨ reducible e σ.
 
-  (* This (weak) form of atomicity is enough to open invariants when WP ensures
+  (* [Atomic not_stuck]: This (weak) form of atomicity is enough to open invariants when WP ensures
      safety, i.e., programs never can get stuck.  We have an example in
      lambdaRust of an expression that is atomic in this sense, but not in the
      stronger sense defined below, and we have to be able to open invariants
      around that expression.  See `CasStuckS` in
-     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). *)
-  Class Atomic (e : expr Λ) : Prop :=
-    atomic σ e' σ' efs : prim_step e σ e' σ' efs → irreducible e' σ'.
+     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
 
-  (* To open invariants with a WP that does not ensure safety, we need a
+     [Atomic maybe_stuck]: To open invariants with a WP that does not ensure safety, we need a
      stronger form of atomicity.  With the above definition, in case `e` reduces
      to a stuck non-value, there is no proof that the invariants have been
      established again. *)
-  Class StronglyAtomic (e : expr Λ) : Prop :=
-    strongly_atomic σ e' σ' efs : prim_step e σ e' σ' efs → is_Some (to_val e').
+  Class Atomic (s : stuckness) (e : expr Λ) : Prop :=
+    atomic σ e' σ' efs :
+      prim_step e σ e' σ' efs →
+      if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
 
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
@@ -91,8 +91,8 @@ Section language.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-  Lemma strongly_atomic_atomic e : StronglyAtomic e → Atomic e.
-  Proof. unfold StronglyAtomic, Atomic. eauto using val_irreducible. Qed.
+  Lemma strongly_atomic_atomic e : Atomic maybe_stuck e → Atomic not_stuck e.
+  Proof. unfold Atomic. eauto using val_irreducible. Qed.
 
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 8be71d97bc3cf06e5f6aa74bf906887727c00ba8..aa228e7062321526b85dcb2f940bb261c47ad7e0 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -233,8 +233,8 @@ Qed.
 Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
 Proof. iIntros "H". iApply (wp_strong_mono s E); try iFrame; auto. Qed.
 
-Lemma wp_atomic' s E1 E2 e Φ :
-  StronglyAtomic e ∨ s = not_stuck ∧ Atomic e →
+Lemma wp_strong_atomic s E1 E2 e Φ :
+  Atomic maybe_stuck e →
   (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
 Proof.
   iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
@@ -242,15 +242,25 @@ Proof.
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
-  destruct Hatomic as [Hstrong|[? Hweak]].
-  - destruct (Hstrong _ _ _ _ Hstep) as [v <-%of_to_val].
-    iMod ("H" with "[#]") as "($ & H & $)"; first done.
-    iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
-  - destruct s; last done. iMod ("H" with "[//]") as "(Hphy & H & $)".
-    rewrite !wp_unfold /wp_pre. destruct (to_val e2).
-    + iDestruct "H" as ">> $". by iFrame.
-    + iMod ("H" with "[$]") as "[H _]".
-      iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hweak _ _ _ _ Hstep).
+  destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
+  iMod ("H" with "[#]") as "($ & H & $)"; first done.
+  iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
+Qed.
+
+Lemma wp_weak_atomic E1 E2 e Φ :
+  Atomic not_stuck e →
+  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
+Proof.
+  iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
+  destruct (to_val e) as [v|] eqn:He.
+  { by iDestruct "H" as ">>> $". }
+  iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
+  iMod ("H" with "[//]") as "(Hphy & H & $)".
+  rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
+  - iDestruct "H" as ">> $". by iFrame.
+  - iMod ("H" with "[$]") as "[H _]".
+    iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hatomic _ _ _ _ Hstep).
 Qed.
 
 Lemma wp_step_fupd s E1 E2 e P Φ :
@@ -315,14 +325,9 @@ Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
   (|={E}=> Φ v) ⊢ WP e @ s; E {{ Φ }}.
 Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
 
-Lemma wp_strong_atomic s E1 E2 e Φ :
-  StronglyAtomic e →
+Lemma wp_atomic s E1 E2 e Φ `{!Atomic s e} :
   (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
-Proof. by eauto using wp_atomic'. Qed.
-Lemma wp_atomic E1 E2 e Φ :
-  Atomic e →
-  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
-Proof. by eauto using wp_atomic'. Qed.
+Proof. destruct s. exact: wp_weak_atomic. exact: wp_strong_atomic. Qed.
 
 Lemma wp_frame_l s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
 Proof. iIntros "[??]". iApply (wp_strong_mono s E E _ Φ); try iFrame; eauto. Qed.
@@ -386,16 +391,9 @@ Section proofmode_classes.
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
   (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
-  Global Instance elim_modal_fupd_wp_strong_atomic E1 E2 e P Φ :
-    StronglyAtomic e →
+  Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
+    Atomic s e →
     ElimModal (|={E1,E2}=> P) P
             (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
-  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_strong_atomic. Qed.
-
-  (* lower precedence than elim_modal_fupd_wp_strong_atomic (for no good reason) *)
-  Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
-    Atomic e →
-    ElimModal (|={E1,E2}=> P) P
-            (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 110.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
 End proofmode_classes.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 6834c5c5e3928fd626f706c6eda0a8daf90d433e..b6189d30914b1013507cdb921c9c62f891905c68 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these
 mask changing update modalities directly in our proofs, but in this file we use
 the first prove the rule as a lemma, and then use that. *)
 Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ :
-  nclose N ⊆ E → Atomic e →
+  nclose N ⊆ E → Atomic not_stuck e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".