Collect all relevant atoms for disjunction elimination.
Disj.elim. over non-recursive branches initially. Description of upcoming overhaul: treat unary (invariants -- recursive definitions) and binary (postconditions -- existential types) predicate variables separately. Binary pred vars start from strongest -- will fail if abduction detects they are too weak.