-* If α* is an expression of type *a*, and *u* is a variable of
-*type b*, then *λuα* has type <code><b, a></code>.
+* If *α* is an expression of type *a*, and *u* is a variable of type *b*, then *λuα* has type <code><b, a></code>.