diff --git a/_CoqProject b/_CoqProject
index 5aa77d4016e7cfbb8c81c57f5289d50130504ff5..1dbcef5c7785dd0793e724b595815dbac59223ac 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,7 +5,6 @@ theories/utils/llist.v
 theories/utils/compare.v
 theories/utils/contribution.v
 theories/utils/group.v
-theories/utils/misc.v
 theories/channel/channel.v
 theories/channel/proto_model.v
 theories/channel/proto_channel.v
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index f7bf1dc496237dcb23506c24a8155189f333c2aa..6ae5317db11f4a58bed825fdece0fef5a7b21149 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -17,8 +17,9 @@ and [chan_own]:
   [s] ([Left] or [Right]) has contents [vs]. *)
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
+From iris.heap_lang Require Import lifting.
 From iris.algebra Require Import excl auth list.
-From actris.utils Require Import auth_excl llist misc.
+From actris.utils Require Import auth_excl llist.
 Set Default Proof Using "Type".
 
 Inductive side := Left | Right.
diff --git a/theories/utils/misc.v b/theories/utils/misc.v
deleted file mode 100644
index 86a9f3c13e8553d9af904781f95d54145f70ba10..0000000000000000000000000000000000000000
--- a/theories/utils/misc.v
+++ /dev/null
@@ -1,10 +0,0 @@
-From iris.heap_lang Require Import notation.
-Set Default Proof Using "Type".
-
-(** 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.