prove MK_COMB, EQ_MP, and BETA correct

also, define type_has_meaning to complement has_meaning (as type_ok does
term_ok).
also prove various term constructor/destructor things correct (in the
form of theorems about has_meaning).

remaining inferences to prove correct are ABS, DEDUCT_ANTISYM,
INST{,_TYPE} and the definitional rules. I believe these are in order of
increasing difficulty.