let mk_diseq x y j =
  let (x, y) = Term.orient (x, y) in 
    Trace.msg "fact" "Diseq" (x, y) Term.pp_diseq;
    (x, y, j)