sig
  val mk_const : Sym.t -> Term.t
  val mk_app : Sym.t -> Term.t list -> Term.t
  val destruct : Term.t -> Sym.t * Term.t list
  val sym_of : Term.t -> Sym.t
  val theory_of : Term.t -> Th.t
  val args_of : Term.t -> Term.t list
end