let rec pp fmt = function
  | Equal(x, y, _) ->  Pretty.infix Term.pp "=" Term.pp fmt (x, y)
  | Diseq(x, y, _) ->  Pretty.infix Term.pp "<>" Term.pp fmt (x, y)
  | Cnstrnt(x, c, _) -> Pretty.infix Term.pp "" Sign.pp fmt (x, c)

and pp_equal fmt e = 
  let (x, y, _) = d_equal e in
  Pretty.infix Term.pp "=" Term.pp fmt (x, y)

and pp_diseq fmt d = 
  let (x, y, _) = d_diseq d in
  Pretty.infix Term.pp "<>" Term.pp fmt (x, y)

and pp_cnstrnt fmt c = 
  let (x, i, _) = d_cnstrnt c in
  Pretty.infix Term.pp "" Sign.pp fmt (x, i)