sig
  type t
  val eq : V.t -> V.t -> bool
  val fold : (Term.t -> Term.t * Jst.t -> 'a -> 'a) -> V.t -> 'a -> 'a
  val pp : V.t Pretty.printer
  val find : V.t -> Jst.Eqtrans.t
  val cnstrnt : V.t -> Term.t -> Var.Cnstrnt.t * Jst.t
  val removable : V.t -> Term.Var.Set.t
  val is_equal : V.t -> Term.t -> Term.t -> Jst.t option
  val is_canonical : V.t -> Term.t -> bool
  val empty : V.t
  val is_empty : V.t -> bool
  val copy : V.t -> V.t
  val merge : Fact.Equal.t -> V.t -> unit
  val gc : (Term.t -> bool) -> V.t -> unit
  val garbage_collection_enabled : bool Pervasives.ref
  val accumulate : V.t -> (Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
  val iter : V.t -> (Term.t -> unit) -> Term.t -> unit
  val exists : V.t -> (Term.t -> bool) -> Term.t -> bool
  val for_all : V.t -> (Term.t -> bool) -> Term.t -> bool
  val choose : V.t -> (Term.t -> 'a option) -> Term.t -> 'a
  val diff : V.t -> V.t -> V.t
end