diff --git a/theories/tactics_vProp.v b/theories/tactics_vProp.v
index 0169eb4deaa3efb0955f2e0c172f8db69c5d2d9a..6e085ac59906cbe8380b09d7f1acf0fe82d1f901 100644
--- a/theories/tactics_vProp.v
+++ b/theories/tactics_vProp.v
@@ -5,27 +5,6 @@ From igps Require tactics.
 Import base.
 
 
-Lemma atomic_correct e V : tactics.W.atomic0 e →
-                           Atomic (Λ:=ra_lang) WeaklyAtomic (tactics.W.to_expr' e,V).
-Proof.
-(*   intros He. apply ectx_language_atomic; last first. *)
-(*   - apply ectxi_language_sub_redexes_are_values => /= Ki [e' V'] Hfill. *)
-(*     (destruct e=> //); destruct Ki; repeat (simplify_eq; case_match=>//); *)
-(*     rewrite /= /ra_lang.fill_item /fill_item /= in Hfill; *)
-(*     inversion Hfill; subst; *)
-(*     try rewrite decide_left; eauto. *)
-(*     move: He. rewrite [atomic _]/=. repeat (case_match) => // _. *)
-(*     apply to_val_is_Some'. econstructor.  *)
-(*     naive_solver eauto using to_val_is_Some'. *)
-(*   - intros σ e' σ' ef Hstep; simpl in *. *)
-(*     apply language.val_irreducible; revert Hstep. *)
-(*     destruct e', e => //=. simplify_eq. inversion 1. simplify_eq. *)
-(*     destruct e=> //=; repeat (simplify_eq/=; case_match=>//); *)
-(*       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. *)
-(*     unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto. *)
-(* Qed. *)
-Admitted.
-
 Ltac solve_closed :=
   match goal with
   | |- Closed ?X ?e =>