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