possible induction theorems for type_cmp and term_cmp

not sure how careful the statement of these needs to be for the
translator...