more automation, simple type join written

More small tests for the automation (bamcis). A type join (join) is now
implemented and proven to produce super-types of the two input types.
This (join) was created to help automation: It does not work for super
complex cases obviously, but it nails the simple ones (which make up a
majority of the common cases). Also proved some useful rewrite rules
regarding TT/FF and conjunction/disjunction.