The only types available to you in this flavor of STLC are bool, bool -> bool, bool -> bool -> bool, (bool -> bool) -> bool, etc. Structurally, if `true := \x\

The only types available to you in this flavor of STLC are bool, bool -> bool, bool -> bool -> bool, (bool -> bool) -> bool, etc. Structurally, if `true := \x\y.x`, the simplest attempt at typing it would be `true : bool -> bool -> bool`. But that means `true` can't have type `bool`! What you need is to say that true (like false) chooses one of its two inputs to return, no matter what type that happens to be. So we introduce a type parameter (think Java generics, if that's what you're familiar with). "Given any type T, `true T` has type T -> T -> T". A formalized notation for this (there is more than one notation you'll see) is `true : ∀ (T : Type), T -> T -> T`. And `false` has the same type. This type obviates the need for a declared `bool` type.