Comment about the relation between `discrete_fun` and non-expansive functions.

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.