Every sort-erased theory

Importing a single theory module instead compiles, and adds to smt!, that theory alone.