diff --git a/_CoqProject b/_CoqProject
index e46494d29bd95eeab8cb8432f4ea5d54f5633add..843f066acc79b8e5e9b25720b75aa4983368a4ba 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,7 +8,6 @@
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
 
-theories/utils/skip.v
 theories/utils/llist.v
 theories/utils/compare.v
 theories/utils/contribution.v
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index e8d038eb646fe47d103a085ed50db99b806f82ba..2c53a5efd81612ed04999d4c02582563080c988b 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -25,7 +25,7 @@ From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Export proofmode.
 From iris.heap_lang.lib Require Import spin_lock.
 From actris.channel Require Export proto.
-From actris.utils Require Import llist skip.
+From actris.utils Require Import llist.
 Set Default Proof Using "Type".
 
 Local Existing Instance spin_lock.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 92c4c0041d3c88e7b542315014ac3a0f209ab8c9..9e9dfcfbfc71854310044ceafa0e101b9ac1849d 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -54,10 +54,17 @@ From actris.channel Require Import proto_model.
 Set Default Proof Using "Type".
 Export action.
 
+(** * Types *)
+Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
+Declare Scope proto_scope.
+Delimit Scope proto_scope with proto.
+Bind Scope proto_scope with iProto.
+Open Scope proto.
+
 (** * Setup of Iris's cameras *)
 Class protoG Σ V :=
   protoG_authG ::
-    inG Σ (excl_authR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))).
+    inG Σ (excl_authR (laterO (iProto Σ V))).
 
 Definition protoΣ V := #[
   GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
@@ -65,13 +72,6 @@ Definition protoΣ V := #[
 Global Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
 Proof. solve_inG. Qed.
 
-(** * Types *)
-Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
-Declare Scope proto_scope.
-Delimit Scope proto_scope with proto.
-Bind Scope proto_scope with iProto.
-Open Scope proto.
-
 (** * Messages *)
 Section iMsg.
   Set Primitive Projections.
diff --git a/theories/utils/skip.v b/theories/utils/skip.v
deleted file mode 100644
index 76c38b38bbf5ed7898d402dc1ceb500cf560d710..0000000000000000000000000000000000000000
--- a/theories/utils/skip.v
+++ /dev/null
@@ -1,11 +0,0 @@
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
-
-Definition skipN : val :=
-  rec: "go" "n" := if: #0 < "n" then "go" ("n" - #1) else #().
-
-Lemma skipN_spec `{heapGS Σ} Φ (n : nat) : ▷^n (Φ #()) -∗ WP skipN #n {{ Φ }}.
-Proof.
-  iIntros "HΦ". iInduction n as [|n] "IH"; wp_rec; wp_pures; [done|].
-  rewrite Z.sub_1_r Nat2Z.inj_succ Z.pred_succ. by iApply "IH".
-Qed.