<code>Λ</code> binds type variables instead of expression
variables. So in the expression
-<code>Λ 'a (λ x:'a . x)</code>
+<code>Λ α (λ x:α . x)</code>
the <code>Λ</code> binds the type variable `'a` that occurs in
the <code>λ</code> abstract. Of course, as long as type