let rec mk_diseq (a, b) =
  if Term.eq a b then 
    mk_false
  else if Term.is_interp_const a && Term.is_interp_const b then
    mk_true
  else if Term.eq a Boolean.mk_true then
    mk_equal (b, Boolean.mk_false)
  else if Term.eq a Boolean.mk_false then
    mk_equal (b, Boolean.mk_true)
  else if Term.eq b Boolean.mk_true then
    mk_equal(a, Boolean.mk_false)
  else if Term.eq b Boolean.mk_false then
    mk_equal (a, Boolean.mk_true)
  else
    Diseq(a, b)