QED.Subst
type t = sigma
val create : ?pool:pool -> unit -> t
val copy : sigma -> sigma
val fresh : t -> tau -> var
val find : t -> term -> term
val filter : t -> term -> bool
val add : t -> term -> term -> unit
Must bind lc-closed terms, or raise Invalid_argument
val add_fun : t -> ( term -> term ) -> unit
val add_filter : t -> ( term -> bool ) -> unit
Only modifies terms that pass the filter.
val add_var : t -> var -> unit
To the pool
val add_vars : t -> Vars.t -> unit
val add_term : t -> term -> unit