sig
  type set = Wp.Vset.vset list
  and vset =
      Set of Wp.Lang.F.tau * Wp.Lang.F.term
    | Singleton of Wp.Lang.F.term
    | Range of Wp.Lang.F.term option * Wp.Lang.F.term option
    | Descr of Wp.Lang.F.var list * Wp.Lang.F.term * Wp.Lang.F.pred
  val tau_of_set : Wp.Lang.F.tau -> Wp.Lang.F.tau
  val vars : Wp.Vset.set -> Wp.Lang.F.Vars.t
  val occurs : Wp.Lang.F.var -> Wp.Vset.set -> bool
  val empty : Wp.Vset.set
  val singleton : Wp.Lang.F.term -> Wp.Vset.set
  val range : Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Vset.set
  val union : Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
  val inter : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val member : Wp.Lang.F.term -> Wp.Vset.set -> Wp.Lang.F.pred
  val in_size : Wp.Lang.F.term -> int -> Wp.Lang.F.pred
  val in_range :
    Wp.Lang.F.term ->
    Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.pred
  val sub_range :
    Wp.Lang.F.term ->
    Wp.Lang.F.term ->
    Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.pred
  val ordered :
    limit:bool ->
    strict:bool ->
    Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.pred
  val is_empty : Wp.Vset.set -> Wp.Lang.F.pred
  val equal : Wp.Vset.set -> Wp.Vset.set -> Wp.Lang.F.pred
  val subset : Wp.Vset.set -> Wp.Vset.set -> Wp.Lang.F.pred
  val disjoint : Wp.Vset.set -> Wp.Vset.set -> Wp.Lang.F.pred
  val concretize : Wp.Vset.set -> Wp.Lang.F.term
  val bound_shift :
    Wp.Lang.F.term option -> Wp.Lang.F.term -> Wp.Lang.F.term option
  val bound_add :
    Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.term option
  val bound_sub :
    Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.term option
  val pp_bound : Format.formatter -> Wp.Lang.F.term option -> unit
  val pp_vset : Format.formatter -> Wp.Vset.vset -> unit
  val pretty : Format.formatter -> Wp.Vset.set -> unit
  val map : (Wp.Lang.F.term -> Wp.Lang.F.term) -> Wp.Vset.set -> Wp.Vset.set
  val map_opp : Wp.Vset.set -> Wp.Vset.set
  val lift :
    (Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term) ->
    Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
  val lift_add : Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
  val lift_sub : Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
  val descr :
    Wp.Vset.vset -> Wp.Lang.F.var list * Wp.Lang.F.term * Wp.Lang.F.pred
end