removing some dependencies from unification.
fixing assumption prover.