sig
  type constructor = Term.lsymbol * Term.lsymbol option list
  type data_decl = Ty.tysymbol * Decl.constructor list
  type ls_defn
  type logic_decl = Term.lsymbol * Decl.ls_defn
  val make_ls_defn :
    Term.lsymbol -> Term.vsymbol list -> Term.term -> Decl.logic_decl
  val open_ls_defn : Decl.ls_defn -> Term.vsymbol list * Term.term
  val open_ls_defn_cb :
    Decl.ls_defn ->
    Term.vsymbol list * Term.term *
    (Term.lsymbol -> Term.vsymbol list -> Term.term -> Decl.logic_decl)
  val ls_defn_axiom : Decl.ls_defn -> Term.term
  val ls_defn_of_axiom : Term.term -> Decl.logic_decl option
  val ls_defn_decrease : Decl.ls_defn -> int list
  type call_set
  type vs_graph
  val create_call_set : unit -> Decl.call_set
  val create_vs_graph : Term.vsymbol list -> Decl.vs_graph
  val register_call :
    Decl.call_set ->
    Ident.ident -> Decl.vs_graph -> Ident.ident -> Term.term list -> unit
  val vs_graph_drop : Decl.vs_graph -> Term.vsymbol -> Decl.vs_graph
  val vs_graph_let :
    Decl.vs_graph -> Term.term -> Term.vsymbol -> Decl.vs_graph
  val vs_graph_pat :
    Decl.vs_graph -> Term.term -> Term.pattern -> Decl.vs_graph
  val find_variant : exn -> Decl.call_set -> Ident.ident -> int list
  type prsymbol = private { pr_name : Ident.ident; }
  module Mpr :
    sig
      type key = prsymbol
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  module Spr :
    sig
      module M :
        sig
          type key = prsymbol
          type 'a t = 'a Mpr.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> 'a -> 'a t -> 'a t
          val singleton : key -> 'a -> 'a t
          val remove : key -> 'a t -> 'a t
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val for_all : (key -> 'a -> bool) -> 'a t -> bool
          val exists : (key -> 'a -> bool) -> 'a t -> bool
          val filter : (key -> 'a -> bool) -> 'a t -> 'a t
          val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
          val cardinal : 'a t -> int
          val bindings : 'a t -> (key * 'a) list
          val min_binding : 'a t -> key * 'a
          val max_binding : 'a t -> key * 'a
          val choose : 'a t -> key * 'a
          val split : key -> 'a t -> 'a t * 'a option * 'a t
          val find : key -> 'a t -> 'a
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val set_union : 'a t -> 'a t -> 'a t
          val set_inter : 'a t -> 'b t -> 'a t
          val set_diff : 'a t -> 'b t -> 'a t
          val set_submap : 'a t -> 'b t -> bool
          val set_disjoint : 'a t -> 'b t -> bool
          val set_compare : 'a t -> 'b t -> int
          val set_equal : 'a t -> 'b t -> bool
          val find_def : 'a -> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('a -> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> 'a -> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
          val fold2_inter :
            (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> 'c -> 'c) ->
            'a t -> 'b t -> 'c -> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> 'a -> 'a t -> 'a t
          val replace : exn -> key -> 'a -> 'a t -> 'a t
          val keys : 'a t -> key list
          val values : 'a t -> 'a list
          val of_list : (key * 'a) list -> 'a t
          val contains : 'a t -> key -> bool
          val domain : 'a t -> unit t
          val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = 'a Mpr.enumeration
          val val_enum : 'a enumeration -> (key * 'a) option
          val start_enum : 'a t -> 'a enumeration
          val next_enum : 'a enumeration -> 'a enumeration
          val start_ge_enum : key -> 'a t -> 'a enumeration
          val next_ge_enum : key -> 'a enumeration -> 'a enumeration
        end
      type elt = M.key
      type t = unit M.t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val merge : (elt -> bool -> bool -> bool) -> t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val disjoint : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val change : (bool -> bool) -> elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
      val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val translate : (elt -> elt) -> t -> t
      val add_new : exn -> elt -> t -> t
      val is_num_elt : int -> t -> bool
      val of_list : elt list -> t
      val contains : t -> elt -> bool
      val add_left : t -> elt -> t
      val remove_left : t -> elt -> t
      val print :
        (Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
    end
  module Hpr :
    sig
      type key = prsymbol
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  module Wpr :
    sig
      type key = prsymbol
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val find : 'a t -> key -> 'a
      val mem : 'a t -> key -> bool
      val set : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val length : 'a t -> int
      val memoize : int -> (key -> 'a) -> key -> 'a
      val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
      val memoize_option : int -> (key option -> 'a) -> key option -> 'a
    end
  val create_prsymbol : Ident.preid -> Decl.prsymbol
  val pr_equal : Decl.prsymbol -> Decl.prsymbol -> bool
  val pr_hash : Decl.prsymbol -> int
  type ind_decl = Term.lsymbol * (Decl.prsymbol * Term.term) list
  type ind_sign = Ind | Coind
  type ind_list = Decl.ind_sign * Decl.ind_decl list
  type prop_kind = Plemma | Paxiom | Pgoal
  type prop_decl = Decl.prop_kind * Decl.prsymbol * Term.term
  type decl = private {
    d_node : Decl.decl_node;
    d_news : Ident.Sid.t;
    d_tag : Weakhtbl.tag;
  }
  and decl_node = private
      Dtype of Ty.tysymbol
    | Ddata of Decl.data_decl list
    | Dparam of Term.lsymbol
    | Dlogic of Decl.logic_decl list
    | Dind of Decl.ind_list
    | Dprop of Decl.prop_decl
  module Mdecl :
    sig
      type key = decl
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  module Sdecl :
    sig
      module M :
        sig
          type key = decl
          type 'a t = 'a Mdecl.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> 'a -> 'a t -> 'a t
          val singleton : key -> 'a -> 'a t
          val remove : key -> 'a t -> 'a t
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val for_all : (key -> 'a -> bool) -> 'a t -> bool
          val exists : (key -> 'a -> bool) -> 'a t -> bool
          val filter : (key -> 'a -> bool) -> 'a t -> 'a t
          val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
          val cardinal : 'a t -> int
          val bindings : 'a t -> (key * 'a) list
          val min_binding : 'a t -> key * 'a
          val max_binding : 'a t -> key * 'a
          val choose : 'a t -> key * 'a
          val split : key -> 'a t -> 'a t * 'a option * 'a t
          val find : key -> 'a t -> 'a
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val set_union : 'a t -> 'a t -> 'a t
          val set_inter : 'a t -> 'b t -> 'a t
          val set_diff : 'a t -> 'b t -> 'a t
          val set_submap : 'a t -> 'b t -> bool
          val set_disjoint : 'a t -> 'b t -> bool
          val set_compare : 'a t -> 'b t -> int
          val set_equal : 'a t -> 'b t -> bool
          val find_def : 'a -> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('a -> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> 'a -> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
          val fold2_inter :
            (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> 'c -> 'c) ->
            'a t -> 'b t -> 'c -> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> 'a -> 'a t -> 'a t
          val replace : exn -> key -> 'a -> 'a t -> 'a t
          val keys : 'a t -> key list
          val values : 'a t -> 'a list
          val of_list : (key * 'a) list -> 'a t
          val contains : 'a t -> key -> bool
          val domain : 'a t -> unit t
          val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = 'a Mdecl.enumeration
          val val_enum : 'a enumeration -> (key * 'a) option
          val start_enum : 'a t -> 'a enumeration
          val next_enum : 'a enumeration -> 'a enumeration
          val start_ge_enum : key -> 'a t -> 'a enumeration
          val next_ge_enum : key -> 'a enumeration -> 'a enumeration
        end
      type elt = M.key
      type t = unit M.t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val merge : (elt -> bool -> bool -> bool) -> t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val disjoint : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val change : (bool -> bool) -> elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
      val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val translate : (elt -> elt) -> t -> t
      val add_new : exn -> elt -> t -> t
      val is_num_elt : int -> t -> bool
      val of_list : elt list -> t
      val contains : t -> elt -> bool
      val add_left : t -> elt -> t
      val remove_left : t -> elt -> t
      val print :
        (Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
    end
  module Wdecl :
    sig
      type key = decl
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val find : 'a t -> key -> 'a
      val mem : 'a t -> key -> bool
      val set : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val length : 'a t -> int
      val memoize : int -> (key -> 'a) -> key -> 'a
      val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
      val memoize_option : int -> (key option -> 'a) -> key option -> 'a
    end
  module Hdecl :
    sig
      type key = decl
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  val d_equal : Decl.decl -> Decl.decl -> bool
  val d_hash : Decl.decl -> int
  val create_ty_decl : Ty.tysymbol -> Decl.decl
  val create_data_decl : Decl.data_decl list -> Decl.decl
  val create_param_decl : Term.lsymbol -> Decl.decl
  val create_logic_decl : Decl.logic_decl list -> Decl.decl
  val create_ind_decl : Decl.ind_sign -> Decl.ind_decl list -> Decl.decl
  val create_prop_decl :
    Decl.prop_kind -> Decl.prsymbol -> Term.term -> Decl.decl
  val get_used_syms_ty : Ty.ty -> Ident.Sid.t
  val get_used_syms_decl : Decl.decl -> Ident.Sid.t
  exception IllegalTypeAlias of Ty.tysymbol
  exception NonPositiveTypeDecl of Ty.tysymbol * Term.lsymbol * Ty.ty
  exception InvalidIndDecl of Term.lsymbol * Decl.prsymbol
  exception NonPositiveIndDecl of Term.lsymbol * Decl.prsymbol * Term.lsymbol
  exception NoTerminationProof of Term.lsymbol
  exception BadLogicDecl of Term.lsymbol * Term.lsymbol
  exception UnboundVar of Term.vsymbol
  exception ClashIdent of Ident.ident
  exception EmptyDecl
  exception EmptyAlgDecl of Ty.tysymbol
  exception EmptyIndDecl of Term.lsymbol
  exception BadConstructor of Term.lsymbol
  exception BadRecordField of Term.lsymbol
  exception BadRecordCons of Term.lsymbol * Ty.tysymbol
  exception BadRecordType of Term.lsymbol * Ty.tysymbol
  exception BadRecordUnnamed of Term.lsymbol * Ty.tysymbol
  exception RecordFieldMissing of Term.lsymbol
  exception DuplicateRecordField of Term.lsymbol
  exception UnexpectedProjOrConstr of Term.lsymbol
  val decl_map : (Term.term -> Term.term) -> Decl.decl -> Decl.decl
  val decl_fold : ('a -> Term.term -> 'a) -> 'a -> Decl.decl -> 'a
  val decl_map_fold :
    ('a -> Term.term -> 'a * Term.term) -> 'a -> Decl.decl -> 'a * Decl.decl
  module DeclTF :
    sig
      val decl_map :
        (Term.term -> Term.term) ->
        (Term.term -> Term.term) -> Decl.decl -> Decl.decl
      val decl_fold :
        ('a -> Term.term -> 'a) ->
        ('a -> Term.term -> 'a) -> 'a -> Decl.decl -> 'a
      val decl_map_fold :
        ('a -> Term.term -> 'a * Term.term) ->
        ('a -> Term.term -> 'a * Term.term) ->
        'a -> Decl.decl -> 'a * Decl.decl
    end
  type known_map = Decl.decl Ident.Mid.t
  val known_id : Decl.known_map -> Ident.ident -> unit
  val known_add_decl : Decl.known_map -> Decl.decl -> Decl.known_map
  val merge_known : Decl.known_map -> Decl.known_map -> Decl.known_map
  exception KnownIdent of Ident.ident
  exception UnknownIdent of Ident.ident
  exception RedeclaredIdent of Ident.ident
  exception NonFoundedTypeDecl of Ty.tysymbol
  val find_constructors :
    Decl.known_map -> Ty.tysymbol -> Decl.constructor list
  val find_inductive_cases :
    Decl.known_map -> Term.lsymbol -> (Decl.prsymbol * Term.term) list
  val find_logic_definition :
    Decl.known_map -> Term.lsymbol -> Decl.ls_defn option
  val find_prop : Decl.known_map -> Decl.prsymbol -> Term.term
  val find_prop_decl :
    Decl.known_map -> Decl.prsymbol -> Decl.prop_kind * Term.term
  exception EmptyRecord
  val parse_record :
    Decl.known_map ->
    (Term.lsymbol * 'a) list ->
    Term.lsymbol * Term.lsymbol list * 'a Term.Mls.t
  val make_record :
    Decl.known_map -> (Term.lsymbol * Term.term) list -> Ty.ty -> Term.term
  val make_record_update :
    Decl.known_map ->
    Term.term -> (Term.lsymbol * Term.term) list -> Ty.ty -> Term.term
  val make_record_pattern :
    Decl.known_map ->
    (Term.lsymbol * Term.pattern) list -> Ty.ty -> Term.pattern
end