-*and* occurs inside of the definition. System F does not have
-recursion. The third problem is more subtle. The defintion as given
-takes two types as parameters: the type of the first argument expected
-by each conjunct, and the type of the result of applying each conjunct
-to an argument of that type. We would like to instantiate the
-recursive use of *and* in the definition by using the result type.
-But fully instantiating the definition as given requires type
-application to a pair of types, not just one type.
+*and* occurs inside of the definition. We know how to handle some
+cases of using a function name inside of its own definition in the
+untyped lambda calculus, but System F does not have
+recursion. [Exercise: convince yourself that the fixed-point
+combinator `Y` can't be typed in System F.]
+
+The third problem is more subtle. The defintion as given takes two
+types as parameters: the type of the first argument expected by each
+conjunct, and the type of the result of applying each conjunct to an
+argument of that type. We would like to instantiate the recursive use
+of *and* in the definition by using the result type, so that
+"<code>and [β]</code>" evaluates to the kind of *and* that
+coordinates expressions of type β. But fully instantiating the
+definition as given requires type application to a *pair* of types,
+not to just to a single type. We want to somehow guarantee that β
+will always itself be a complex type. This goes beyond the expressive
+power of System F.