-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.
+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 to just a single type. We want to somehow
+guarantee that 'b will always itself be a complex type.