let is_interp = function
  | App((Arith _ | Bv _), _) -> true
  | _ -> false