In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type <code><u>Q</u></code> is <code><u>bool</u></code>).
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 arrow as
+if `α list` is our box type, we can write the second type as:
<code><u>int</u> -> <u>int list</u></code>