sig
  val th : Th.t
  val map : (Term.t -> Term.t) -> Term.t -> Term.t
  val solve : Fact.Equal.t -> Fact.Equal.t list
  val disjunction : Fact.Equal.t -> Clause.t
end