of type `'a`. In general, then, the type of the unapplied
(polymorphic) identity function is
-<code>(Λ 'a (λ x:'a . x)): (∀ 'a . 'a -> 'a)
+<code>(Λ 'a (λ x:'a . x)): (∀ 'a . 'a -> 'a)</code>
Pred in System F
----------------