Factorize constraint for the body of a definition out of a disjunction over existential type eliminations. Fix to reversing universally quantified variables. More logging.