simplification replaces constraints by simpler constraints while preserving logical equivalence
propagation adds new constraints which are logically redundant but may cause further simplification
the LHS builtin constraints are a precondition on the applicability of the rule
only rewrite RHS user constraints in a simplification rule