let of_equal (a, b, rho) = (Atom.mk_equal (a, b), rho)