diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 2c82031da1ddcda2e3e13a6c4ab7b769433b559a..9ed9b22e42242f62ba2b99a3259d7693505514be 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -17,7 +17,10 @@ In this file we define the three message-passing connectives:
   polarity of the endpoints.
 - [send] takes an endpoint and adds an element to the first buffer.
 - [recv] performs a busy loop until there is something in the second buffer,
-  which it pops and returns, locking during each peek.*)
+  which it pops and returns, locking during each peek.
+
+It is additionaly shown that the channel ownership [c ↣ prot] is closed under
+the subprotocol relation [⊑] *)
 From iris.heap_lang Require Export lifting notation.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib Require Import spin_lock.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 012eb277df831e975aba2238a5441df404b8ada6..f483fa042b941e5e6970dfeb31114ca842b791b8 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -27,7 +27,7 @@ Futhermore, we define the following operations:
 - [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa
 - [iProto_app], which appends two protocols as described in proto_model.v
 
-In addition we define the [iProto_le] subprotocol relation, which generalises
+In addition we define the subprotocol relation [iProto_le] [⊑], which generalises
 the following inductive definition for asynchronous subtyping on session types:
 
                  p1 <: p2           p1 <: p2          p1 <: !B.p3    ?A.p3 <: p2