let is_interp = function
  | Term.App(sym, _, _) -> Sym.theory_of sym = Th.p
  | _ -> false