diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index d80dec80b826ce13e0d3bd59b228e34548fd88ff..5b9f3533a9378e2942eecfbe13c68044f5ed5300 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -43,10 +43,11 @@ Definition start_chan : val := λ: "f",
 Definition send : val :=
   λ: "c" "v",
     let: "lk" := Snd "c" in
-    acquire "lk";;
     let: "l" := Fst (Fst "c") in
+    let: "r" := Snd (Fst "c") in
+    acquire "lk";;
     lsnoc "l" "v";;
-    skipN (llength (Snd (Fst "c")));; (* "Ghost" operation for later stripping *)
+    skipN (llength "r");; (* "Ghost" operation for later stripping *)
     release "lk".
 
 Definition try_recv : val :=
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 4190a724864d2207f01c9f413a59202d51dc7eb7..f6b965f03ef71f7e25fb25f50a6fccc32aaa725d 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -708,6 +708,7 @@ Section proto.
     - iApply iProto_le_recv. iIntros (v' p') "(->&Hp&$) !>".
       iExists p2. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
   Qed.
+
   Lemma iProto_le_base_swap v1 v2 P1 P2 p :
     ⊢ (<?> MSG v1 {{ P1 }}; <!> MSG v2 {{ P2 }}; p)
     ⊑ (<!> MSG v2 {{ P2 }}; <?> MSG v1 {{ P1 }}; p).
@@ -1297,6 +1298,7 @@ Section proto.
     FromModal (modality_instances.modality_laterN 1) (p1 ⊑ p2)
               ((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2).
   Proof. apply iProto_le_base. Qed.
+
 End proto.
 
 Typeclasses Opaque iProto_ctx iProto_own.
diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index b6dbab1bf43aa9d1583a4dfd2653b1c0a79f763a..d828053d1b4eac7c439cda594f95e890e71004ea 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -1,5 +1,4 @@
 From actris.channel Require Import proofmode proto channel.
-From actris.logrel Require Import subtyping_rules.
 From iris.proofmode Require Import tactics.
 From actris.utils Require Import llist.