Further tidying.

In particular, TCP1_lemSupport now has HOL mapping for almost all
constants that are declared with "val". The exception is "SET_CHOOSE",
which should map directly to HOL's choice operator @.