Revert part of separation changes: include abduction answer, with instance parameters renamed to formal parameters, in binary pred var solution. Better old-new parameter matching in `converge`. Small cosmetic changes.
In disjunction elimination result, add/preserve redundant equalities for better connected component semantics.
Filter initial postconditions through validity check; the check is not sufficient yet to fix the problem.