inline TypeDecls during SMT translation

Since we've resolved all types at this point, it seems straightforward to simply
emit the underlying type of a TypeExprID instead of just the ID. This should let
us (1) trivially support any kind of TypeExprID and (2) support SMT solvers that
don't understand define-sort, which we would have had to use going forwards.