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