Forbid injections into hooked sorts #1731
Description
Sort injections into hooked sorts are invalid for the same reason that constructor declarations in hooked sorts are invalid. We should check this whenever we validate an axiom with the subsort attribute.