let
of_diseq (a, b, rho) = (
Atom
.mk_diseq (a, b), rho)