diff --git a/_CoqProject b/_CoqProject
index 11274648c017781f5618f9ed962582a8f503c62d..54eb66339c6873fd8f95976deb3f8238c3f30d28 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,6 +5,7 @@ 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 29271fd9d64458a0e2065d347c13b147e14cb9dc..2a396eb396a59b46a58549801eb28db96bf20d84 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -18,7 +18,7 @@ and [chan_own]:
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import excl auth list.
-From actris.utils Require Import auth_excl llist.
+From actris.utils Require Import auth_excl llist misc.
 Set Default Proof Using "Type".
 
 Inductive side := Left | Right.
@@ -75,6 +75,7 @@ Proof.
     |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
 Qed.
 
+
 Section channel.
   Context `{!heapG Σ, !chanG Σ} (N : namespace).
 
@@ -126,9 +127,9 @@ Section channel.
     wp_lam.
     wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
     wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
-    iMod (own_alloc (● (to_auth_excl [])  ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
     { by apply auth_both_valid. }
-    iMod (own_alloc (● (to_auth_excl [])  ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
     { by apply auth_both_valid. }
     wp_apply (newlock_spec N (∃ ls rs,
       llist sbi_internal_eq l ls ∗ own lsγ (● to_auth_excl ls) ∗
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index da6ebdff702c2f71ba67480f80da1c549c9da9d5..a1418229d4ed5fbc6c505182b0e0c1ae745e453b 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -15,8 +15,7 @@ depends on the communicated value V and the dependent tail
 propositions of the logic.
 
 The type is defined as a solution to a recursive domain
-equation, as it is self-referential under the guard of â–¶.
-*)
+equation, as it is self-referential under the guard of â–¶.*)
 
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
diff --git a/theories/utils/misc.v b/theories/utils/misc.v
new file mode 100644
index 0000000000000000000000000000000000000000..86a9f3c13e8553d9af904781f95d54145f70ba10
--- /dev/null
+++ b/theories/utils/misc.v
@@ -0,0 +1,10 @@
+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.