let is_uninterp = function
  | App(sym, _, _) -> Sym.theory_of sym = Th.u
  | _ -> false