sig
  type vsymbol = private { vs_name : Ident.ident; vs_ty : Ty.ty; }
  module Mvs :
    sig
      type key = vsymbol
      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 Svs :
    sig
      module M :
        sig
          type key = vsymbol
          type 'a t = 'a Mvs.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 Mvs.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 Hvs :
    sig
      type key = vsymbol
      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 Wvs :
    sig
      type key = vsymbol
      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 vs_compare : Term.vsymbol -> Term.vsymbol -> int
  val vs_equal : Term.vsymbol -> Term.vsymbol -> bool
  val vs_hash : Term.vsymbol -> int
  val create_vsymbol : Ident.preid -> Ty.ty -> Term.vsymbol
  type lsymbol = private {
    ls_name : Ident.ident;
    ls_args : Ty.ty list;
    ls_value : Ty.ty option;
    ls_constr : int;
    ls_proj : bool;
  }
  module Mls :
    sig
      type key = lsymbol
      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 Sls :
    sig
      module M :
        sig
          type key = lsymbol
          type 'a t = 'a Mls.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 Mls.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 Hls :
    sig
      type key = lsymbol
      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 Wls :
    sig
      type key = lsymbol
      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 ls_compare : Term.lsymbol -> Term.lsymbol -> int
  val ls_equal : Term.lsymbol -> Term.lsymbol -> bool
  val ls_hash : Term.lsymbol -> int
  val create_lsymbol :
    ?constr:int ->
    ?proj:bool -> Ident.preid -> Ty.ty list -> Ty.ty option -> Term.lsymbol
  val create_fsymbol :
    ?constr:int ->
    ?proj:bool -> Ident.preid -> Ty.ty list -> Ty.ty -> Term.lsymbol
  val create_psymbol : Ident.preid -> Ty.ty list -> Term.lsymbol
  val ls_ty_freevars : Term.lsymbol -> Ty.Stv.t
  exception EmptyCase
  exception DuplicateVar of Term.vsymbol
  exception UncoveredVar of Term.vsymbol
  exception BadArity of Term.lsymbol * int
  exception FunctionSymbolExpected of Term.lsymbol
  exception PredicateSymbolExpected of Term.lsymbol
  exception ConstructorExpected of Term.lsymbol
  exception InvalidIntegerLiteralType of Ty.ty
  exception InvalidRealLiteralType of Ty.ty
  exception InvalidStringLiteralType of Ty.ty
  type pattern = private {
    pat_node : Term.pattern_node;
    pat_vars : Term.Svs.t;
    pat_ty : Ty.ty;
  }
  and pattern_node =
      Pwild
    | Pvar of Term.vsymbol
    | Papp of Term.lsymbol * Term.pattern list
    | Por of Term.pattern * Term.pattern
    | Pas of Term.pattern * Term.vsymbol
  val pat_wild : Ty.ty -> Term.pattern
  val pat_var : Term.vsymbol -> Term.pattern
  val pat_app : Term.lsymbol -> Term.pattern list -> Ty.ty -> Term.pattern
  val pat_or : Term.pattern -> Term.pattern -> Term.pattern
  val pat_as : Term.pattern -> Term.vsymbol -> Term.pattern
  val pat_map :
    (Term.pattern -> Term.pattern) -> Term.pattern -> Term.pattern
  val pat_fold : ('a -> Term.pattern -> 'a) -> 'a -> Term.pattern -> 'a
  val pat_all : (Term.pattern -> bool) -> Term.pattern -> bool
  val pat_any : (Term.pattern -> bool) -> Term.pattern -> bool
  type quant = Tforall | Texists
  type binop = Tand | Tor | Timplies | Tiff
  type term = private {
    t_node : Term.term_node;
    t_ty : Ty.ty option;
    t_attrs : Ident.Sattr.t;
    t_loc : Loc.position option;
  }
  and term_node =
      Tvar of Term.vsymbol
    | Tconst of Constant.constant
    | Tapp of Term.lsymbol * Term.term list
    | Tif of Term.term * Term.term * Term.term
    | Tlet of Term.term * Term.term_bound
    | Tcase of Term.term * Term.term_branch list
    | Teps of Term.term_bound
    | Tquant of Term.quant * Term.term_quant
    | Tbinop of Term.binop * Term.term * Term.term
    | Tnot of Term.term
    | Ttrue
    | Tfalse
  and term_bound
  and term_branch
  and term_quant
  and trigger = Term.term list list
  val term_size : Term.term -> int
  val term_branch_size : Term.term_branch -> int
  val t_hash_generic :
    trigger:bool -> attr:bool -> const:bool -> Term.term -> int
  val t_compare_generic :
    trigger:bool ->
    attr:bool -> loc:bool -> const:bool -> Term.term -> Term.term -> int
  val t_equal_generic :
    trigger:bool ->
    attr:bool -> loc:bool -> const:bool -> Term.term -> Term.term -> bool
  val mterm_generic :
    trigger:bool ->
    attr:bool ->
    loc:bool -> const:bool -> (module Extmap.S with type key = Term.term)
  val sterm_generic :
    trigger:bool ->
    attr:bool ->
    loc:bool -> const:bool -> (module Extset.S with type M.key = Term.term)
  val hterm_generic :
    trigger:bool ->
    attr:bool ->
    loc:bool -> const:bool -> (module Exthtbl.S with type key = Term.term)
  val t_equal_strict : Term.term -> Term.term -> bool
  val t_compare_strict : Term.term -> Term.term -> int
  val t_hash_strict : Term.term -> int
  module Mterm_strict :
    sig
      type key = term
      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 Sterm_strict :
    sig
      module M :
        sig
          type key = term
          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
      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 Hterm_strict :
    sig
      type key = term
      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 t_equal : Term.term -> Term.term -> bool
  val t_compare : Term.term -> Term.term -> int
  val t_hash : Term.term -> int
  module Mterm :
    sig
      type key = term
      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 Sterm :
    sig
      module M :
        sig
          type key = term
          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
      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 Hterm :
    sig
      type key = term
      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 t_close_bound : Term.vsymbol -> Term.term -> Term.term_bound
  val t_close_branch : Term.pattern -> Term.term -> Term.term_branch
  val t_close_quant :
    Term.vsymbol list -> Term.trigger -> Term.term -> Term.term_quant
  val t_open_bound : Term.term_bound -> Term.vsymbol * Term.term
  val t_open_branch : Term.term_branch -> Term.pattern * Term.term
  val t_open_quant :
    Term.term_quant -> Term.vsymbol list * Term.trigger * Term.term
  val t_open_bound_with : Term.term -> Term.term_bound -> Term.term
  val t_clone_bound_id :
    ?loc:Loc.position ->
    ?attrs:Ident.Sattr.t -> Term.term_bound -> Ident.preid
  val t_open_bound_cb :
    Term.term_bound ->
    Term.vsymbol * Term.term * (Term.vsymbol -> Term.term -> Term.term_bound)
  val t_open_branch_cb :
    Term.term_branch ->
    Term.pattern * Term.term *
    (Term.pattern -> Term.term -> Term.term_branch)
  val t_open_quant_cb :
    Term.term_quant ->
    Term.vsymbol list * Term.trigger * Term.term *
    (Term.vsymbol list -> Term.trigger -> Term.term -> Term.term_quant)
  val t_peek_bound : Term.term_bound -> Ident.ident
  val t_peek_branch : Term.term_branch -> Ident.Sid.t
  val t_peek_quant : Term.term_quant -> Ident.ident list
  exception TermExpected of Term.term
  exception FmlaExpected of Term.term
  val t_type : Term.term -> Ty.ty
  val t_prop : Term.term -> Term.term
  val t_ty_check : Term.term -> Ty.ty option -> unit
  val t_app : Term.lsymbol -> Term.term list -> Ty.ty option -> Term.term
  val fs_app : Term.lsymbol -> Term.term list -> Ty.ty -> Term.term
  val ps_app : Term.lsymbol -> Term.term list -> Term.term
  val t_app_infer : Term.lsymbol -> Term.term list -> Term.term
  val ls_arg_inst : Term.lsymbol -> Term.term list -> Ty.ty Ty.Mtv.t
  val ls_app_inst :
    Term.lsymbol -> Term.term list -> Ty.ty option -> Ty.ty Ty.Mtv.t
  val check_literal : Constant.constant -> Ty.ty -> unit
  val t_var : Term.vsymbol -> Term.term
  val t_const : Constant.constant -> Ty.ty -> Term.term
  val t_if : Term.term -> Term.term -> Term.term -> Term.term
  val t_let : Term.term -> Term.term_bound -> Term.term
  val t_case : Term.term -> Term.term_branch list -> Term.term
  val t_eps : Term.term_bound -> Term.term
  val t_quant : Term.quant -> Term.term_quant -> Term.term
  val t_forall : Term.term_quant -> Term.term
  val t_exists : Term.term_quant -> Term.term
  val t_binary : Term.binop -> Term.term -> Term.term -> Term.term
  val t_and : Term.term -> Term.term -> Term.term
  val t_or : Term.term -> Term.term -> Term.term
  val t_implies : Term.term -> Term.term -> Term.term
  val t_iff : Term.term -> Term.term -> Term.term
  val t_not : Term.term -> Term.term
  val t_true : Term.term
  val t_false : Term.term
  val t_nat_const : int -> Term.term
  val t_int_const : BigInt.t -> Term.term
  val t_real_const :
    ?pow2:BigInt.t -> ?pow5:BigInt.t -> BigInt.t -> Term.term
  val t_string_const : string -> Term.term
  val stop_split : Ident.attribute
  val asym_split : Ident.attribute
  val t_and_l : Term.term list -> Term.term
  val t_or_l : Term.term list -> Term.term
  val t_and_asym : Term.term -> Term.term -> Term.term
  val t_or_asym : Term.term -> Term.term -> Term.term
  val t_and_asym_l : Term.term list -> Term.term
  val t_or_asym_l : Term.term list -> Term.term
  val t_let_close : Term.vsymbol -> Term.term -> Term.term -> Term.term
  val t_eps_close : Term.vsymbol -> Term.term -> Term.term
  val t_case_close :
    Term.term -> (Term.pattern * Term.term) list -> Term.term
  val t_quant_close :
    Term.quant -> Term.vsymbol list -> Term.trigger -> Term.term -> Term.term
  val t_forall_close :
    Term.vsymbol list -> Term.trigger -> Term.term -> Term.term
  val t_exists_close :
    Term.vsymbol list -> Term.trigger -> Term.term -> Term.term
  val t_attr_set :
    ?loc:Loc.position -> Ident.Sattr.t -> Term.term -> Term.term
  val t_attr_add : Ident.attribute -> Term.term -> Term.term
  val t_attr_remove : Ident.attribute -> Term.term -> Term.term
  val t_attr_copy : Term.term -> Term.term -> Term.term
  val t_let_close_simp : Term.vsymbol -> Term.term -> Term.term -> Term.term
  val t_let_close_simp_keep_var :
    keep:bool -> Term.vsymbol -> Term.term -> Term.term -> Term.term
  val t_if_simp : Term.term -> Term.term -> Term.term -> Term.term
  val t_let_simp : Term.term -> Term.term_bound -> Term.term
  val t_let_simp_keep_var :
    keep:bool -> Term.term -> Term.term_bound -> Term.term
  val t_case_simp : Term.term -> Term.term_branch list -> Term.term
  val t_quant_simp : Term.quant -> Term.term_quant -> Term.term
  val t_forall_simp : Term.term_quant -> Term.term
  val t_exists_simp : Term.term_quant -> Term.term
  val t_binary_simp : Term.binop -> Term.term -> Term.term -> Term.term
  val t_and_simp : Term.term -> Term.term -> Term.term
  val t_and_simp_l : Term.term list -> Term.term
  val t_or_simp : Term.term -> Term.term -> Term.term
  val t_or_simp_l : Term.term list -> Term.term
  val t_implies_simp : Term.term -> Term.term -> Term.term
  val t_iff_simp : Term.term -> Term.term -> Term.term
  val t_not_simp : Term.term -> Term.term
  val t_and_asym_simp : Term.term -> Term.term -> Term.term
  val t_and_asym_simp_l : Term.term list -> Term.term
  val t_or_asym_simp : Term.term -> Term.term -> Term.term
  val t_or_asym_simp_l : Term.term list -> Term.term
  val t_case_close_simp :
    Term.term -> (Term.pattern * Term.term) list -> Term.term
  val t_quant_close_simp :
    Term.quant -> Term.vsymbol list -> Term.trigger -> Term.term -> Term.term
  val t_forall_close_simp :
    Term.vsymbol list -> Term.trigger -> Term.term -> Term.term
  val t_exists_close_simp :
    Term.vsymbol list -> Term.trigger -> Term.term -> Term.term
  val t_forall_close_merge : Term.vsymbol list -> Term.term -> Term.term
  val t_exists_close_merge : Term.vsymbol list -> Term.term -> Term.term
  val ps_equ : Term.lsymbol
  val t_equ : Term.term -> Term.term -> Term.term
  val t_neq : Term.term -> Term.term -> Term.term
  val t_equ_simp : Term.term -> Term.term -> Term.term
  val t_neq_simp : Term.term -> Term.term -> Term.term
  val ps_ignore : Term.lsymbol
  val fs_bool_true : Term.lsymbol
  val fs_bool_false : Term.lsymbol
  val t_bool_true : Term.term
  val t_bool_false : Term.term
  val to_prop : Term.term -> Term.term
  val fs_tuple : int -> Term.lsymbol
  val t_tuple : Term.term list -> Term.term
  val is_fs_tuple : Term.lsymbol -> bool
  val is_fs_tuple_id : Ident.ident -> int option
  val fs_func_app : Term.lsymbol
  val t_func_app : Term.term -> Term.term -> Term.term
  val t_pred_app : Term.term -> Term.term -> Term.term
  val t_func_app_l : Term.term -> Term.term list -> Term.term
  val t_pred_app_l : Term.term -> Term.term list -> Term.term
  val ps_acc : Term.lsymbol
  val ps_wf : Term.lsymbol
  val t_lambda : Term.vsymbol list -> Term.trigger -> Term.term -> Term.term
  val t_open_lambda :
    Term.term -> Term.vsymbol list * Term.trigger * Term.term
  val t_open_lambda_cb :
    Term.term ->
    Term.vsymbol list * Term.trigger * Term.term *
    (Term.vsymbol list -> Term.trigger -> Term.term -> Term.term)
  val t_is_lambda : Term.term -> bool
  val t_closure : Term.lsymbol -> Ty.ty list -> Ty.ty option -> Term.term
  val t_app_partial :
    Term.lsymbol -> Term.term list -> Ty.ty list -> Ty.ty option -> Term.term
  val t_func_app_beta : Term.term -> Term.term -> Term.term
  val t_pred_app_beta : Term.term -> Term.term -> Term.term
  val t_func_app_beta_l : Term.term -> Term.term list -> Term.term
  val t_pred_app_beta_l : Term.term -> Term.term list -> Term.term
  val t_map : (Term.term -> Term.term) -> Term.term -> Term.term
  val t_fold : ('a -> Term.term -> 'a) -> 'a -> Term.term -> 'a
  val t_iter : (Term.term -> unit) -> Term.term -> unit
  val t_map_fold :
    ('a -> Term.term -> 'a * Term.term) -> 'a -> Term.term -> 'a * Term.term
  val t_all : (Term.term -> bool) -> Term.term -> bool
  val t_any : (Term.term -> bool) -> Term.term -> bool
  val t_map_simp : (Term.term -> Term.term) -> Term.term -> Term.term
  val t_map_sign :
    (bool -> Term.term -> Term.term) -> bool -> Term.term -> Term.term
  val t_map_cont :
    ((Term.term -> 'a) -> Term.term -> 'a) ->
    (Term.term -> 'a) -> Term.term -> 'a
  val list_map_cont :
    (('a -> 'b) -> 'c -> 'b) -> ('a list -> 'b) -> 'c list -> 'b
  val tr_equal : Term.trigger -> Term.trigger -> bool
  val tr_map : (Term.term -> Term.term) -> Term.trigger -> Term.trigger
  val tr_fold : ('a -> Term.term -> 'a) -> 'a -> Term.trigger -> 'a
  val tr_map_fold :
    ('a -> Term.term -> 'a * Term.term) ->
    'a -> Term.trigger -> 'a * Term.trigger
  module TermTF :
    sig
      val t_select :
        (Term.term -> 'a) -> (Term.term -> 'a) -> Term.term -> 'a
      val t_selecti :
        ('a -> Term.term -> 'b) ->
        ('a -> Term.term -> 'b) -> 'a -> Term.term -> 'b
      val t_map :
        (Term.term -> Term.term) ->
        (Term.term -> Term.term) -> Term.term -> Term.term
      val t_fold :
        ('a -> Term.term -> 'a) ->
        ('a -> Term.term -> 'a) -> 'a -> Term.term -> 'a
      val t_map_fold :
        ('a -> Term.term -> 'a * Term.term) ->
        ('a -> Term.term -> 'a * Term.term) ->
        'a -> Term.term -> 'a * Term.term
      val t_all :
        (Term.term -> bool) -> (Term.term -> bool) -> Term.term -> bool
      val t_any :
        (Term.term -> bool) -> (Term.term -> bool) -> Term.term -> bool
      val t_map_simp :
        (Term.term -> Term.term) ->
        (Term.term -> Term.term) -> Term.term -> Term.term
      val t_map_sign :
        (bool -> Term.term -> Term.term) ->
        (bool -> Term.term -> Term.term) -> bool -> Term.term -> Term.term
      val t_map_cont :
        ((Term.term -> 'a) -> Term.term -> 'a) ->
        ((Term.term -> 'a) -> Term.term -> 'a) ->
        (Term.term -> 'a) -> Term.term -> 'a
      val tr_map :
        (Term.term -> Term.term) ->
        (Term.term -> Term.term) -> Term.trigger -> Term.trigger
      val tr_fold :
        ('a -> Term.term -> 'a) ->
        ('a -> Term.term -> 'a) -> 'a -> Term.trigger -> 'a
      val tr_map_fold :
        ('a -> Term.term -> 'a * Term.term) ->
        ('a -> Term.term -> 'a * Term.term) ->
        'a -> Term.trigger -> 'a * Term.trigger
    end
  val t_v_map : (Term.vsymbol -> Term.term) -> Term.term -> Term.term
  val t_v_fold : ('a -> Term.vsymbol -> 'a) -> 'a -> Term.term -> 'a
  val t_v_all : (Term.vsymbol -> bool) -> Term.term -> bool
  val t_v_any : (Term.vsymbol -> bool) -> Term.term -> bool
  val t_v_count : ('a -> Term.vsymbol -> int -> 'a) -> 'a -> Term.term -> 'a
  val t_v_occurs : Term.vsymbol -> Term.term -> int
  val t_subst_single : Term.vsymbol -> Term.term -> Term.term -> Term.term
  val t_subst : Term.term Term.Mvs.t -> Term.term -> Term.term
  val t_ty_subst :
    Ty.ty Ty.Mtv.t -> Term.term Term.Mvs.t -> Term.term -> Term.term
  val t_subst_types :
    Ty.ty Ty.Mtv.t ->
    Term.term Term.Mvs.t -> Term.term -> Term.term Term.Mvs.t * Term.term
  val t_closed : Term.term -> bool
  val t_vars : Term.term -> int Term.Mvs.t
  val t_freevars : int Term.Mvs.t -> Term.term -> int Term.Mvs.t
  val t_ty_freevars : Ty.Stv.t -> Term.term -> Ty.Stv.t
  val t_gen_map :
    (Ty.ty -> Ty.ty) ->
    (Term.lsymbol -> Term.lsymbol) ->
    Term.vsymbol Term.Mvs.t -> Term.term -> Term.term
  val t_s_map :
    (Ty.ty -> Ty.ty) ->
    (Term.lsymbol -> Term.lsymbol) -> Term.term -> Term.term
  val t_s_fold :
    ('a -> Ty.ty -> 'a) ->
    ('a -> Term.lsymbol -> 'a) -> 'a -> Term.term -> 'a
  val t_s_all :
    (Ty.ty -> bool) -> (Term.lsymbol -> bool) -> Term.term -> bool
  val t_s_any :
    (Ty.ty -> bool) -> (Term.lsymbol -> bool) -> Term.term -> bool
  val t_ty_map : (Ty.ty -> Ty.ty) -> Term.term -> Term.term
  val t_ty_fold : ('a -> Ty.ty -> 'a) -> 'a -> Term.term -> 'a
  val t_app_map :
    (Term.lsymbol -> Ty.ty list -> Ty.ty option -> Term.lsymbol) ->
    Term.term -> Term.term
  val t_app_fold :
    ('a -> Term.lsymbol -> Ty.ty list -> Ty.ty option -> 'a) ->
    'a -> Term.term -> 'a
  val t_case_fold :
    ('a -> Ty.tysymbol -> Ty.ty list -> Ty.ty option -> 'a) ->
    'a -> Term.term -> 'a
  val t_occurs : Term.term -> Term.term -> bool
  val t_replace : Term.term -> Term.term -> Term.term -> Term.term
  val remove_unused_in_term : bool -> Term.term -> Term.term
end