export the term_welltyped theorem
define subterm/subtype and rename has_meaning_subterm

to has_meaning_VFREE_IN, since subterm is actually slightly different
attempt to add type destructor rules to syntax

but proving the resulting obligation in the semantics seems very
difficult. giving up temporarily in favour of exploring the completely
syntactic route further..
export type_ok_Bool theorem
extend proves_IMP to show term/type_ok implies context_ok
RTC_subterm_Const for stateless
rename term_ok_welltyped to term_ok_Comb_welltyped
has_meaning_subterm