I have to admit that I am out of my field, so help me a bit, you expressed that it must be dependently typed because false and true are a -> b -> a|b under union (and a->b->b and a->b->a respectively) so the the abstractions can take any functions subtyping a->b->a|b, thus to make them correct you need dependent types to verify that the abstractions take only True and False?
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.
Is this correct?