sig
  type t = Lang.F.Tset.t Lang.F.Vmap.t
  val empty : 'Lang.F.Vmap.t
  val merge :
    Lang.F.Tset.t Lang.F.Vmap.t ->
    Lang.F.Tset.t Lang.F.Vmap.t -> Lang.F.Tset.t Lang.F.Vmap.t
  val add_def :
    Letify.Defs.t Pervasives.ref ->
    Lang.F.Vmap.key -> Lang.F.Tset.elt -> unit
  val diff :
    Lang.F.term list -> Lang.F.var -> Lang.F.term list -> Lang.F.term list
  val add_linear :
    Letify.Defs.t Pervasives.ref ->
    Lang.F.Vmap.key -> Lang.F.term list -> Lang.F.term list -> unit
  val terms : Lang.F.term -> Lang.F.term list
  val atoms : Lang.F.term list -> Lang.F.var list
  val defs : Letify.Defs.t Pervasives.ref -> Lang.F.term -> unit
  val defs_affine :
    Letify.Defs.t Pervasives.ref ->
    Lang.F.Tset.elt -> Lang.F.Tset.elt -> unit
  val defs_eq :
    Letify.Defs.t Pervasives.ref ->
    Lang.F.Tset.elt -> Lang.F.Tset.elt -> unit
  val extract : Lang.F.pred -> Letify.Defs.t
  val domain : 'Lang.F.Vmap.t -> Lang.F.Vars.t
end