sig
  val is_interp : Term.t -> bool
  val is_pure : Term.t -> bool
  val mk_cons : Term.t -> Term.t -> Term.t
  val mk_car : Term.t -> Term.t
  val mk_cdr : Term.t -> Term.t
  val mk_tuple : Term.t list -> Term.t
  val mk_proj : int -> Term.t -> Term.t
  val map : (Term.t -> Term.t) -> Term.t -> Term.t
  val apply : Term.Equal.t -> Term.t -> Term.t
  val sigma : Sym.product -> Term.t list -> Term.t
  val solve : Term.Equal.t -> Term.Equal.t list
end