let is_equal a b =
  if eq a b then
    Three.Yes
  else match a, b with                                 (* constants from within a theory are *)
    | App((Arith _ as c), []), App((Arith _ as d), []) (* assumed to interpreted differently *)
        when not(Sym.eq c d) -> Three.No
    | App((Bv _ as c), []), App((Bv _ as d), [])
        when not(Sym.eq c d) -> Three.No
    | _ ->
        Three.X