let mk_equal x y j =
  let (x, y) = Term.orient (x, y) in
    Trace.msg "fact" "Equal" (x, y) Term.pp_equal;
    (x, y, j)