Sort well-formedness

SMT-term type checker

Typed Term denotation

Type-checking inversion lemmas (consumed by Term.denoteTyped)