diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 5cafc8f7b5cda3be5d31391615092867a4a182fc..1789ca57080da7b48708345567d2701eafcaed5f 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -195,9 +195,7 @@ Definition is_atomic (e : expr) :=
   end.
 Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
 Proof.
-  enough (is_atomic e → Atomic StronglyAtomic (to_expr e)).
-  { destruct s; auto using strongly_atomic_atomic. }
-  intros He. apply ectx_language_atomic.
+  intros He. apply strongly_atomic_atomic, ectx_language_atomic.
   - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
     destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 26f813c5f55797ec836638ee85968fa61eb58554..707f9c671861cf99218208bf490f352c8637849f 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -109,9 +109,9 @@ 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 :
-    Atomic StronglyAtomic e → Atomic WeaklyAtomic e.
-  Proof. unfold Atomic. eauto using val_irreducible. Qed.
+  Lemma strongly_atomic_atomic e a :
+    Atomic StronglyAtomic e → Atomic a e.
+  Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
 
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.