What was its purpose in the first place? Integers are protected
in Simplify anyway and then we can simply forget the difference
between the infinite sorts (as we do in encoding_tptp).