let is_equal a b =
  if eq a b then Three.Yes else 
    match a, b with                
      | App(c, [], _), App(d, [], _) 
          when Sym.theory_of c = Sym.theory_of d 
            && not(Th.is_uninterpreted (Sym.theory_of c))
            -> Three.No
      | _ -> 
          Three.X