let pp_diseq fmt (x,y) = 
  Pretty.infix pp "<>" pp fmt (x,y)