Lambda the Ultimate

Hi everyone,
I've been learning a small amount of type theory lately. I've noticed, as I'm sure most people have, that types in the typed lambda calculus always seem to be "determinable", I'm not sure what the correct term for it is. What I mean is this: a type is a ground type, or an arrow type, such that when applied to a term of the correct type, the type on the right of the arrow is also "determinable". For example, the following types are determinable:

Boolean (because it is a ground type)
a -> a
a -> b -> a

But these are not:
a
a -> b

Could someone point me in the right direction as to what to call this property, or if it even necessarily holds, and better yet, how to *prove* that it holds? Thanks!
-Kevin