Operators for Unification and Most General Instance