sig
  val d_interp : Term.t -> Sym.cl * Term.t list
  val mk_apply : Term.t -> Term.t -> Term.t
  val mk_s : unit -> Term.t
  val mk_k : unit -> Term.t
  val mk_i : unit -> Term.t
  val mk_c : unit -> Term.t
  val abstract : Name.t -> Term.t -> Term.t
  val sigma : Sym.cl -> Term.t list -> Term.t
  val map : (Term.t -> Term.t) -> Term.t -> Term.t
  val apply : Term.t * Term.t -> Term.t -> Term.t
  val disapply : Term.t * Term.t -> Term.t -> Term.t
  val solve : Term.Equal.t -> Term.Equal.t list
end