Major conceptual bug fix in unification under quantifier prefix; more rethinking/cleanup needed. Missing tests and small test corrections.