different implementation of Unifier which is more general. Rename before unifing to avoid same names during unification