Prune rather than simplify postconditions, only simplify a bit in `simplify_dsjelim`, substituting-out some variables but not existential variables that are LHSes of min/max atoms. More error-proof handling of variable comparison in `NumS`.