sig
  type t = (Term.trm * Term.trm) list
  val pp : Term.Subst.t Pretty.printer
  val empty : Term.Subst.t
  val fuse :
    Term.apply -> Term.trm * Term.trm -> Term.Subst.t -> Term.Subst.t
  val compose :
    Term.apply -> Term.trm * Term.trm -> Term.Subst.t -> Term.Subst.t
  val lookup : Term.Subst.t -> Term.trm -> Term.trm
  val invlookup : Term.Subst.t -> (Term.trm -> bool) -> Term.trm
  val apply :
    Term.map ->
    ((Term.trm * Term.trm) * 'a) list -> Term.trm -> Term.trm * 'a list
  val fold : (Term.trm * Term.trm -> 'a -> 'a) -> Term.Subst.t -> 'a -> 'a
end