diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index c84bced7cb6954a678858662193ccb2a20b35888..61dc5698696761f3f7da82d7d198b1a0e2a89093 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1103,9 +1103,12 @@ Proof.
destruct n as [|n]; simpl in *; first done. apply oFunctor_ne, Hfg.
Qed.
-(* Dependently-typed functions over a discrete domain *)
-(* We make [discrete_fun] a definition so that we can register it as a canonical
-structure. *)
+(** Dependently-typed functions over a discrete domain *)
+(** We make [discrete_fun] a definition so that we can register it as a
+canonical structure. Note that non-dependent functions over a discrete domain,
+[discrete_fun (λ _, A) B] (or [A -d> B] following the notation we introduce
+below) are isomorphic to [leibnizC A -n> B]. In other words, since the domain
+is discrete, we get non-expansiveness for free. *)
Definition discrete_fun {A} (B : A → ofeT) := ∀ x : A, B x.
Section discrete_fun.