unification algorithms in CuTT