-Note that the left-hand schema `P` is permitted to itself be a boxed type. That is, where if `α list` is our box type, we can write the second type as:
+Note that the left-hand schema `P` is permitted to itself be a boxed
+type. That is, if `α list` is our box type, and `P` is to boxed type
+`int list`, we can write the boxed type that has `P` as its left-hand
+side as