sig
  type cst = Ind_cst.t
  type term = Logtk.FOTerm.t
  type case
  type t
  module Case :
    sig
      type t = Cover_set.case
      val equal : Cover_set.Case.t -> Cover_set.Case.t -> bool
      val compare : Cover_set.Case.t -> Cover_set.Case.t -> int
      val hash : Cover_set.Case.t -> int
      val pp : Cover_set.Case.t CCFormat.printer
      val is_rec : Cover_set.Case.t -> bool
      val is_base : Cover_set.Case.t -> bool
      val to_term : Cover_set.Case.t -> Cover_set.term
      val to_lit : Cover_set.Case.t -> Logtk.Literal.t
      val same_cst : Cover_set.Case.t -> Cover_set.Case.t -> bool
      val sub_constants : Cover_set.Case.t -> Cover_set.cst list
      val skolems : Cover_set.Case.t -> (Logtk.ID.t * Logtk.Type.t) list
    end
  val pp : Cover_set.t CCFormat.printer
  val ty : Cover_set.t -> Logtk.Type.t
  val top : Cover_set.t -> Cover_set.cst
  val declarations : Cover_set.t -> (Logtk.ID.t * Logtk.Type.t) Sequence.t
  val cases :
    ?which:[ `All | `Base | `Rec ] ->
    Cover_set.t -> Cover_set.case Sequence.t
  val sub_constants : Cover_set.t -> Cover_set.cst Sequence.t
  val make : ?cover_set_depth:int -> depth:int -> Logtk.Type.t -> Cover_set.t
end