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 t -> 'a t
      val singleton : key -> '-> '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 option) -> 'a t -> 'a t -> 'a t
      val compare : ('-> '-> int) -> 'a t -> 'a t -> int
      val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val for_all : (key -> '-> bool) -> 'a t -> bool
      val exists : (key -> '-> bool) -> 'a t -> bool
      val filter : (key -> '-> bool) -> 'a t -> 'a t
      val partition : (key -> '-> 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 : ('-> 'b) -> 'a t -> 'b t
      val mapi : (key -> '-> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> '-> '-> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> '-> '-> 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 : '-> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('-> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> '-> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> '-> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> '-> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('-> key -> '-> 'b) -> '-> 'a t -> 'b
      val fold2_inter :
        (key -> '-> '-> '-> 'c) -> 'a t -> 'b t -> '-> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> '-> 'c) ->
        'a t -> 'b t -> '-> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> '-> 'a t -> 'a t
      val replace : exn -> key -> '-> '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 -> '-> 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 = 'Mvs.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> '-> 'a t -> 'a t
          val singleton : key -> '-> '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 option) -> 'a t -> 'a t -> 'a t
          val compare : ('-> '-> int) -> 'a t -> 'a t -> int
          val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
          val for_all : (key -> '-> bool) -> 'a t -> bool
          val exists : (key -> '-> bool) -> 'a t -> bool
          val filter : (key -> '-> bool) -> 'a t -> 'a t
          val partition : (key -> '-> 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 : ('-> 'b) -> 'a t -> 'b t
          val mapi : (key -> '-> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> '-> '-> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> '-> '-> 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 : '-> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('-> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> '-> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> '-> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> '-> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('-> key -> '-> 'b) -> '-> 'a t -> 'b
          val fold2_inter :
            (key -> '-> '-> '-> 'c) -> 'a t -> 'b t -> '-> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> '-> 'c) ->
            'a t -> 'b t -> '-> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> '-> 'a t -> 'a t
          val replace : exn -> key -> '-> '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 -> '-> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = '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) -> t -> '-> '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 : ('-> elt -> 'b) -> '-> t -> 'b
      val fold2_inter : (elt -> '-> 'a) -> t -> t -> '-> 'a
      val fold2_union : (elt -> '-> 'a) -> t -> t -> '-> '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 -> '-> 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 -> '-> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val find_def : 'a t -> '-> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> '-> '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 -> '-> unit
      val remove : 'a t -> key -> unit
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val iterk : (key -> unit) -> 'a t -> unit
      val foldk : (key -> '-> 'b) -> 'a t -> '-> 'b
      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;
  }
  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 t -> 'a t
      val singleton : key -> '-> '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 option) -> 'a t -> 'a t -> 'a t
      val compare : ('-> '-> int) -> 'a t -> 'a t -> int
      val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val for_all : (key -> '-> bool) -> 'a t -> bool
      val exists : (key -> '-> bool) -> 'a t -> bool
      val filter : (key -> '-> bool) -> 'a t -> 'a t
      val partition : (key -> '-> 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 : ('-> 'b) -> 'a t -> 'b t
      val mapi : (key -> '-> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> '-> '-> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> '-> '-> 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 : '-> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('-> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> '-> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> '-> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> '-> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('-> key -> '-> 'b) -> '-> 'a t -> 'b
      val fold2_inter :
        (key -> '-> '-> '-> 'c) -> 'a t -> 'b t -> '-> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> '-> 'c) ->
        'a t -> 'b t -> '-> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> '-> 'a t -> 'a t
      val replace : exn -> key -> '-> '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 -> '-> 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 = 'Mls.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> '-> 'a t -> 'a t
          val singleton : key -> '-> '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 option) -> 'a t -> 'a t -> 'a t
          val compare : ('-> '-> int) -> 'a t -> 'a t -> int
          val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
          val for_all : (key -> '-> bool) -> 'a t -> bool
          val exists : (key -> '-> bool) -> 'a t -> bool
          val filter : (key -> '-> bool) -> 'a t -> 'a t
          val partition : (key -> '-> 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 : ('-> 'b) -> 'a t -> 'b t
          val mapi : (key -> '-> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> '-> '-> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> '-> '-> 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 : '-> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('-> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> '-> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> '-> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> '-> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('-> key -> '-> 'b) -> '-> 'a t -> 'b
          val fold2_inter :
            (key -> '-> '-> '-> 'c) -> 'a t -> 'b t -> '-> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> '-> 'c) ->
            'a t -> 'b t -> '-> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> '-> 'a t -> 'a t
          val replace : exn -> key -> '-> '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 -> '-> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = '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) -> t -> '-> '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 : ('-> elt -> 'b) -> '-> t -> 'b
      val fold2_inter : (elt -> '-> 'a) -> t -> t -> '-> 'a
      val fold2_union : (elt -> '-> 'a) -> t -> t -> '-> '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 -> '-> 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 -> '-> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val find_def : 'a t -> '-> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> '-> '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 -> '-> unit
      val remove : 'a t -> key -> unit
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val iterk : (key -> unit) -> 'a t -> unit
      val foldk : (key -> '-> 'b) -> 'a t -> '-> 'b
      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 -> Ident.preid -> Ty.ty list -> Ty.ty option -> Term.lsymbol
  val create_fsymbol :
    ?constr:int -> 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
  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 : ('-> Term.pattern -> '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 Number.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
  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 t -> 'a t
      val singleton : key -> '-> '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 option) -> 'a t -> 'a t -> 'a t
      val compare : ('-> '-> int) -> 'a t -> 'a t -> int
      val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val for_all : (key -> '-> bool) -> 'a t -> bool
      val exists : (key -> '-> bool) -> 'a t -> bool
      val filter : (key -> '-> bool) -> 'a t -> 'a t
      val partition : (key -> '-> 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 : ('-> 'b) -> 'a t -> 'b t
      val mapi : (key -> '-> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> '-> '-> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> '-> '-> 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 : '-> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('-> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> '-> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> '-> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> '-> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('-> key -> '-> 'b) -> '-> 'a t -> 'b
      val fold2_inter :
        (key -> '-> '-> '-> 'c) -> 'a t -> 'b t -> '-> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> '-> 'c) ->
        'a t -> 'b t -> '-> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> '-> 'a t -> 'a t
      val replace : exn -> key -> '-> '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 -> '-> 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 = 'Mterm.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> '-> 'a t -> 'a t
          val singleton : key -> '-> '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 option) -> 'a t -> 'a t -> 'a t
          val compare : ('-> '-> int) -> 'a t -> 'a t -> int
          val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
          val for_all : (key -> '-> bool) -> 'a t -> bool
          val exists : (key -> '-> bool) -> 'a t -> bool
          val filter : (key -> '-> bool) -> 'a t -> 'a t
          val partition : (key -> '-> 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 : ('-> 'b) -> 'a t -> 'b t
          val mapi : (key -> '-> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> '-> '-> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> '-> '-> 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 : '-> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('-> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> '-> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> '-> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> '-> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('-> key -> '-> 'b) -> '-> 'a t -> 'b
          val fold2_inter :
            (key -> '-> '-> '-> 'c) -> 'a t -> 'b t -> '-> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> '-> 'c) ->
            'a t -> 'b t -> '-> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> '-> 'a t -> 'a t
          val replace : exn -> key -> '-> '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 -> '-> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = 'Mterm.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) -> t -> '-> '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 : ('-> elt -> 'b) -> '-> t -> 'b
      val fold2_inter : (elt -> '-> 'a) -> t -> t -> '-> 'a
      val fold2_union : (elt -> '-> 'a) -> t -> t -> '-> '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 -> '-> 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 -> '-> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val find_def : 'a t -> '-> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> '-> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  val t_compare : Term.term -> Term.term -> int
  val t_equal : Term.term -> Term.term -> bool
  val t_hash : Term.term -> int
  val t_equal_nt_na : Term.term -> Term.term -> bool
  module Hterm_nt_na :
    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 -> '-> 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 -> '-> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val find_def : 'a t -> '-> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> '-> '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 : 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)
  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 : Number.constant -> Ty.ty -> unit
  val t_var : Term.vsymbol -> Term.term
  val t_const : Number.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_bigint_const : BigInt.t -> 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_if_simp : Term.term -> Term.term -> Term.term -> Term.term
  val t_let_simp : 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_let_close_simp : Term.vsymbol -> Term.term -> Term.term -> 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 fs_bool_true : Term.lsymbol
  val fs_bool_false : Term.lsymbol
  val t_bool_true : Term.term
  val t_bool_false : 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 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 : ('-> Term.term -> 'a) -> '-> Term.term -> 'a
  val t_iter : (Term.term -> unit) -> Term.term -> unit
  val t_map_fold :
    ('-> Term.term -> 'a * Term.term) -> '-> 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 :
    (('-> 'b) -> '-> '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 : ('-> Term.term -> 'a) -> '-> Term.trigger -> 'a
  val tr_map_fold :
    ('-> Term.term -> 'a * Term.term) ->
    '-> Term.trigger -> 'a * Term.trigger
  module TermTF :
    sig
      val t_select :
        (Term.term -> 'a) -> (Term.term -> 'a) -> Term.term -> 'a
      val t_selecti :
        ('-> Term.term -> 'b) ->
        ('-> Term.term -> 'b) -> '-> Term.term -> 'b
      val t_map :
        (Term.term -> Term.term) ->
        (Term.term -> Term.term) -> Term.term -> Term.term
      val t_fold :
        ('-> Term.term -> 'a) ->
        ('-> Term.term -> 'a) -> '-> Term.term -> 'a
      val t_map_fold :
        ('-> Term.term -> 'a * Term.term) ->
        ('-> Term.term -> 'a * Term.term) ->
        '-> 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 :
        ('-> Term.term -> 'a) ->
        ('-> Term.term -> 'a) -> '-> Term.trigger -> 'a
      val tr_map_fold :
        ('-> Term.term -> 'a * Term.term) ->
        ('-> Term.term -> 'a * Term.term) ->
        '-> Term.trigger -> 'a * Term.trigger
    end
  val t_v_map : (Term.vsymbol -> Term.term) -> Term.term -> Term.term
  val t_v_fold : ('-> Term.vsymbol -> '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 : ('-> Term.vsymbol -> int -> '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 :
    ('-> Ty.ty -> 'a) ->
    ('-> Term.lsymbol -> '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 : ('-> Ty.ty -> '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 :
    ('-> Term.lsymbol -> Ty.ty list -> Ty.ty option -> 'a) ->
    '-> Term.term -> 'a
  val t_occurs : Term.term -> Term.term -> bool
  val t_replace : Term.term -> Term.term -> Term.term -> Term.term
end