let mk_diseq (a, b) =
  if Term.eq a b then mk_false else
    if Boolean.is_true a then
      mk_equal (b, (Boolean.mk_false()))
    else if Boolean.is_false a then
      mk_equal (b, (Boolean.mk_true()))
    else if Boolean.is_true b then
      mk_equal (a, (Boolean.mk_false()))
    else if Boolean.is_false b then
      mk_equal (a, (Boolean.mk_true()))
    else
      of_diseq (Term.orient (a, b))