refactor: unification now works with two (optional) DB environments
in which bound variables of both terms live.
matching: parameter ?allow_open is now used properly in rewriting and indexing