It enhances the simply-typed lambda calculus with quantification over
types. In System F, you can say things like
-<code>Γ α (\x.x):(α -> α)</code>
+<code>Λ α (\x.x):(α -> α)</code>
This says that the identity function maps arguments of type α to
-results of type α, for any choice of α. So the Γ is
+results of type α, for any choice of α. So the Λ is
a universal quantifier over types.