sig
  val is_empty : Term.t -> bool
  val exists : Arith.Monomials.pred -> Term.t -> bool
  val for_all : Arith.Monomials.pred -> Term.t -> bool
  val fold : (Mpa.Q.t -> Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
  val iter : (Mpa.Q.t -> Term.t -> unit) -> Term.t -> unit
  val mem : Term.t -> Term.t -> bool
  val variable_choose : (Mpa.Q.t -> Term.t -> bool) -> Term.t -> Term.t
  val variable_least_of : Term.t -> Term.t
  val coefficient_of : Term.t -> Term.t -> Mpa.Q.t
end