proofs 1-3 very simple... dealing w/ subsumption

So, it turns out with the simple typing rules written as they are you
end up needing subsumption *all over the place* — for example, any time
you’re reasoning about bools and an explicit #t or #f appears it’s very
possible you’ll need to use subsumption to make things work, since
although both #t and #f *are* bools, they are not equal to bool (since
#t is of type tTrue, #f is of type tFalse, and bool is (tUnion tTrue
tFalse). This makes building Ltac tactics which automatically solve
these “simple examples” more difficult than would be ideal, since often
applying the “fitting relational constructor” leads you directly down a
path where equality is required =(

Saving now… may look into making all typing judgements resort to
subtype checking instead of the current practice of all being literal
(i.e. using equality) and allowing for subsumption when necessary.
We’ll see…