more congruence rules for subsort checking
simplify subsort checking