sig
  val th : Th.t
  val map : (Term.t -> Term.t) -> Term.t -> Term.t
  val sigma : Sym.t -> Term.t list -> Term.t
  val of_equal : Fact.Equal.t -> Can.config -> Fact.Equal.t list
  val of_var_equal : Fact.Equal.t -> Can.config -> Fact.Equal.t list
  val of_var_diseq : Fact.Diseq.t -> Can.config -> Fact.Equal.t list
  val disjunction : Can.config -> Clause.t
end