o introduced some automatic simplification of expressions (true ∧ x ≡
x, etc)
o added the axiom concerning the set of all the values of a given type
backups