sig
  val fnd : Th.t -> Context.t -> Term.t -> Term.t
  val findequiv : Th.t -> Context.t -> Term.t -> Term.t
  val term : Context.t -> Term.t -> Term.t
  val can : Context.t -> Term.t -> Term.t
  val pprod : Context.t -> Sym.pprod -> Term.t list -> Term.t
  val unsigned : Context.t -> Term.t -> Term.t
  val arith : Context.t -> Sym.arith -> Term.t list -> Term.t
  val eq : t -> Term.t -> Term.t -> bool
  val atom : Context.t -> Atom.t -> Atom.t
  val equal : Context.t -> Term.t * Term.t -> Atom.t
  val diseq : Context.t -> Term.t * Term.t -> Atom.t
  val crossmultiply : Context.t -> Term.t * Term.t -> Term.t * Term.t
  val crossmultiply1 : Context.t -> Term.t * Term.t -> Term.t * Term.t
  val sign : Context.t -> Term.t * Sign.t -> Atom.t
  val eq : Context.t -> Term.t -> Term.t -> bool
end