diff --git a/theories/typing/function.v b/theories/typing/function.v
index 44a158ad9a347d0f72abf1849ebacfd75c87a61a..5bf2834649e50884b76e31939835bd1217648ab7 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -15,6 +15,11 @@ Section fn.
                     ty.(ty_wf_E) ++ ty.(ty_outlives_E) ϝ)
        tys ty.
 
+  (* The other alternative for defining the fn type would be to state
+     that the value applied to its parameters is a typed body whose type
+     is the return type.
+     That would be slightly simpler, but, unfortunately, we are no longer
+     able to prove that this is contractive. *)
   Program Definition fn (fp : A → fn_params) : type :=
     {| st_own tid vl := (∃ fb kb xb e H,
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗