sig
  val atom : Context.t * Atom.t -> Context.t * Atom.t
  val equal : Context.t -> Term.t * Term.t -> Context.t * Atom.t
  val diseq : Context.t -> Term.t * Term.t -> Context.t * Atom.t
  val cnstrnt : Context.t -> Term.t * Sign.t -> Context.t * Atom.t
  val term : Th.t -> Context.t * Term.t -> Context.t * Term.t
  val args : Th.t -> Context.t * Term.t list -> Context.t * Term.t list
end