let mk_equal (a, b) =
  if Term.eq a b then mk_true else
    of_equal (Term.orient(a, b))