What every sort-erased theory needs

Terms and values, the Boolean connectives, bound variables, the solver and symbol structures.