Fix
Expression simplification (0 - x) + y --> y - x
Explain test
Prepare state matching for eliminating redundant (often diverging) refinements of `unknown` choices