diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 2a396eb396a59b46a58549801eb28db96bf20d84..f7bf1dc496237dcb23506c24a8155189f333c2aa 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -67,15 +67,6 @@ Definition chanΣ : gFunctors :=
 Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
-(** MOVE TO IRIS *)
-Global Instance fst_atomic a v1 v2 : Atomic a (Fst (v1,v2)%V).
-Proof.
-  apply strongly_atomic_atomic, ectx_language_atomic;
-    [inversion 1; naive_solver
-    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
-Qed.
-
-
 Section channel.
   Context `{!heapG Σ, !chanG Σ} (N : namespace).