diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index b943466e4f0f5fdee26b3d2838ec5ccd936b3b36..a04a43f210e10d904a30d682a7a67f4407b59735 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -9,14 +9,14 @@ The main difference is that the protocols are defined over predicates,
 in place of types.
 
 Dependent Separation Protocols are modelled as the following type:
-- [proto] := 1 + ([action] * (V → (▶ [proto] → PROP) → PROP))
+- [proto := 1 + (action * (V → (▶ proto → PROP) → PROP))]
 
 Here the left-hand side of the sum is used for the terminated process,
 while the right-hand side is used for the communication constructors.
 [action] is an inductively defined datatype with two constructors,
 that is used to differentiate between sending and received, rather than
 having two distinct sums in [proto].
-- [action] := [Send] | [Receive]
+- [action := Send | Receive]
 
 The remainder (V → (▶ [proto] → PROP) → PROP)) is a continuation that
 depends on the communicated value V and the dependent tail (▶ proto → PROP)
diff --git a/theories/utils/auth_excl.v b/theories/utils/auth_excl.v
index 952adadce11fd59ad810e593875d308ab1e7086d..c9e35187c39a970f26ce3cf089e8f6cc84c69c34 100644
--- a/theories/utils/auth_excl.v
+++ b/theories/utils/auth_excl.v
@@ -1,5 +1,11 @@
 (** This file provides utility for defining and using
-the commonly used ghost functor over authoritative exclusive ownership. *)
+a commonly used ghost functor over authoritative exclusive ownership.
+[AuthExcl A := Auth (Option (Excl A))]
+
+This is isomorphic to a half-ownership, with an intuitive
+use-case, being putting the authoritative part in an
+invariant, while giving the other fragment to the client
+with write permissions.  *)
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl auth.
 From iris.base_logic.lib Require Import own.
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 15cb3efd783a0f2c1c094f1bfb63920d9f6f8549..f5213aaffbc9c23f736b3ec8292081cee02dbbd0 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -1,14 +1,12 @@
 (** This file defines a ghost functor for tracking
 "contributions" made to a shared concurrent effort.
 It is ultimately defined as:
-contribution := Auth (Option ((Pos * A) + Excl 1))
-
-Intuitively it allows one to allocate a [server] and
-a number of [client] fragments. The server keeps track
-of the number of active clients, and what resources they
-are currently holding.
-To deallocate a client it must hold no resources.
-To deallocate a server there must be no remaining clients.
+[contribution := Auth (Option ((Pos * A) + Excl 1))]
+
+Intuitively it allows one to allocate a [server] and a
+number of [client] fragments, where the server keeps
+track of the number of active clients, and what resources
+they are currently holding.
 *)
 From iris.base_logic Require Export base_logic lib.iprop lib.own.
 From iris.proofmode Require Export tactics.