sig
  val is_interp : Term.t -> bool
  val is_pure : Term.t -> bool
  val is_diseq : Term.t -> Term.t -> bool
  val mk_inl : Term.t -> Term.t
  val mk_inr : Term.t -> Term.t
  val mk_outl : Term.t -> Term.t
  val mk_outr : Term.t -> Term.t
  val mk_inj : int -> Term.t -> Term.t
  val mk_out : 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.coproduct -> Term.t list -> Term.t
  val solve : Term.t * Term.t -> (Term.t * Term.t) list
end