sig val terms : Reasoner.Clause.t -> Reasoner.term Sequence.t val vars : Reasoner.Clause.t -> Reasoner.ty Libzipperposition.Var.t Sequence.t end