re-factor higher-order unification; much more modular, things are appropriately postponed