sig
  val terms : ArithLit.t -> ArithLit.term Sequence.t
  val vars : ArithLit.t -> Libzipperposition.FOTerm.var Sequence.t
  val to_multiset : ArithLit.t -> (ArithLit.term * Z.t) Sequence.t
end