functor (T : TI.S) ->
  sig
    module U :
      sig
        type t_ = T.t
        val head_sym : t_ -> TI.id
        val to_seq : t_ -> t_ Sequence.t
        val to_seq_vars : t_ -> t_ Var.t Sequence.t
        val to_seq_consts : t_ -> ID.t Sequence.t
        module VarSet :
          sig
            type elt = t_ Var.t
            type t = TermInner.Util(T).VarSet.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 union : t -> t -> t
            val inter : t -> t -> t
            val diff : t -> t -> t
            val compare : t -> t -> int
            val equal : t -> t -> bool
            val subset : 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 find : elt -> t -> elt
            val of_seq : elt CCSet.sequence -> t
            val add_seq : t -> elt CCSet.sequence -> t
            val to_seq : t -> elt CCSet.sequence
            val of_list : elt list -> t
            val add_list : t -> elt list -> t
            val to_list : t -> elt list
            val pp :
              ?start:string ->
              ?stop:string ->
              ?sep:string -> elt CCSet.printer -> t CCSet.printer
            val print :
              ?start:string ->
              ?stop:string ->
              ?sep:string -> elt CCSet.formatter -> t CCSet.formatter
          end
        val to_seq_free_vars : ?bound:VarSet.t -> t_ -> t_ Var.t Sequence.t
        val free_vars : ?bound:VarSet.t -> t_ -> VarSet.t
        val is_var : t_ -> bool
        val is_const : t_ -> bool
        val is_closed : t_ -> bool
        val is_undefined : t_ -> bool
        val free_meta_vars :
          ?init:t_ MetaVar.t ID.Map.t -> t_ -> t_ MetaVar.t ID.Map.t
        val bind_unfold : TI.Binder.t -> t_ -> t_ Var.t list * t_
        val fun_unfold : t_ -> t_ Var.t list * t_
        val get_ty_arg : t_ -> int -> t_ option
        val ty_unfold : t_ -> t_ Var.t list * t_ list * t_
        val ty_is_Type : t_ -> bool
        val ty_returns_Type : t_ -> bool
        val ty_returns_Prop : t_ -> bool
        val ty_returns : t_ -> t_
        val ty_is_Kind : t_ -> bool
        val ty_is_Prop : t_ -> bool
        val ty_is_unitype : t_ -> bool
        val ty_num_param : t_ -> int
        val build : t_ TI.view -> t_
        val const : TI.id -> t_
        val builtin : t_ TI.Builtin.t -> t_
        val app_builtin : t_ TI.Builtin.t -> t_ list -> t_
        val var : t_ TI.var -> t_
        val app : t_ -> t_ list -> t_
        val app_const : ID.t -> t_ list -> t_
        val fun_ : t_ TI.var -> t_ -> t_
        val mu : t_ TI.var -> t_ -> t_
        val let_ : t_ TI.var -> t_ -> t_ -> t_
        val match_with : t_ -> t_ TI.cases -> t_
        val ite : t_ -> t_ -> t_ -> t_
        val forall : t_ TI.var -> t_ -> t_
        val exists : t_ TI.var -> t_ -> t_
        val eq : t_ -> t_ -> t_
        val neq : t_ -> t_ -> t_
        val imply : t_ -> t_ -> t_
        val imply_l : t_ list -> t_ -> t_
        val true_ : t_
        val false_ : t_
        val and_ : t_ list -> t_
        val or_ : t_ list -> t_
        val not_ : t_ -> t_
        val undefined_self : t_ -> t_
        val undefined_atom : ty:t_ -> t_
        val data_test : ID.t -> t_ -> t_
        val data_select : ID.t -> int -> t_ -> t_
        val unparsable : ty:t_ -> t_
        val and_nodup : t_ list -> t_
        val asserting : t_ -> t_ list -> t_
        val assuming : t_ -> t_ list -> t_
        val guard : t_ -> t_ TI.Builtin.guard -> t_
        val mk_bind : TI.Binder.t -> t_ TI.var -> t_ -> t_
        val mk_bind_l : TI.Binder.t -> t_ TI.var list -> t_ -> t_
        val ty_type : t_
        val ty_kind : t_
        val ty_prop : t_
        val ty_unitype : t_
        val ty_builtin : TI.TyBuiltin.t -> t_
        val ty_const : TI.id -> t_
        val ty_app : t_ -> t_ list -> t_
        val ty_arrow : t_ -> t_ -> t_
        val ty_arrow_l : t_ list -> t_ -> t_
        val ty_var : t_ TI.var -> t_
        val ty_meta : t_ MetaVar.t -> t_
        val ty_forall : t_ TI.var -> t_ -> t_
        val fun_l : t_ TI.var list -> t_ -> t_
        val forall_l : t_ TI.var list -> t_ -> t_
        val exists_l : t_ TI.var list -> t_ -> t_
        val ty_forall_l : t_ TI.var list -> t_ -> t_
        val let_l : (t_ TI.var * t_) list -> t_ -> t_
        val close_forall : t_ -> t_
        val hash_fun : t_ CCHash.hash_fun
        val hash : t_ -> int
        val hash_fun_alpha_eq : t_ CCHash.hash_fun
        val hash_alpha_eq : t_ -> int
        val equal : t_ -> t_ -> bool
        module Tbl :
          sig
            type key = t_
            type 'a t = 'a TermInner.Util(T).Tbl.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 fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
            val length : 'a t -> int
            val stats : 'a t -> Hashtbl.statistics
            val get : 'a t -> key -> 'a option
            val get_or : 'a t -> key -> or_:'a -> 'a
            val add_list : 'a list t -> key -> 'a -> unit
            val incr : ?by:int -> int t -> key -> unit
            val decr : ?by:int -> int t -> key -> unit
            val keys : 'a t -> key CCHashtbl.sequence
            val values : 'a t -> 'a CCHashtbl.sequence
            val keys_list : 'a t -> key list
            val values_list : 'a t -> 'a list
            val map_list : (key -> 'a -> 'b) -> 'a t -> 'b list
            val to_seq : 'a t -> (key * 'a) CCHashtbl.sequence
            val of_seq : (key * 'a) CCHashtbl.sequence -> 'a t
            val add_seq : 'a t -> (key * 'a) CCHashtbl.sequence -> unit
            val add_seq_count : int t -> key CCHashtbl.sequence -> unit
            val of_seq_count : key CCHashtbl.sequence -> int t
            val to_list : 'a t -> (key * 'a) list
            val of_list : (key * 'a) list -> 'a t
            val update :
              'a t -> f:(key -> 'a option -> 'a option) -> k:key -> unit
            val print :
              key CCHashtbl.printer ->
              'a CCHashtbl.printer -> 'a t CCHashtbl.printer
          end
        module Map :
          sig
            type key = t_
            type 'a t = 'a TermInner.Util(T).Map.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 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 get : key -> 'a t -> 'a option
            val get_or : key -> 'a t -> or_:'a -> 'a
            val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
            val merge_safe :
              f:(key ->
                 [ `Both of 'a * 'b | `Left of 'a | `Right of 'b ] ->
                 'c option) ->
              'a t -> 'b t -> 'c t
            val of_seq : (key * 'a) CCMap.sequence -> 'a t
            val add_seq : 'a t -> (key * 'a) CCMap.sequence -> 'a t
            val to_seq : 'a t -> (key * 'a) CCMap.sequence
            val of_list : (key * 'a) list -> 'a t
            val add_list : 'a t -> (key * 'a) list -> 'a t
            val keys : 'a t -> key CCMap.sequence
            val values : 'a t -> 'a CCMap.sequence
            val to_list : 'a t -> (key * 'a) list
            val pp :
              ?start:string ->
              ?stop:string ->
              ?arrow:string ->
              ?sep:string ->
              key CCMap.printer -> 'a CCMap.printer -> 'a t CCMap.printer
            val print :
              ?start:string ->
              ?stop:string ->
              ?arrow:string ->
              ?sep:string ->
              key CCMap.formatter ->
              'a CCMap.formatter -> 'a t CCMap.formatter
          end
        val remove_dup : t_ list -> t_ list
        val fold :
          f:('acc -> 'b_acc -> t_ -> 'acc) ->
          bind:('b_acc -> t_ Var.t -> 'b_acc) -> 'acc -> 'b_acc -> t_ -> 'acc
        val iter :
          f:('b_acc -> t_ -> unit) ->
          bind:('b_acc -> t_ Var.t -> 'b_acc) -> 'b_acc -> t_ -> unit
        val map' :
          f:('b_acc -> t_ -> 'a) ->
          bind:('b_acc -> t_ Var.t -> 'b_acc * 'a Var.t) ->
          'b_acc -> t_ -> 'a TI.view
        val map :
          f:('b_acc -> t_ -> t_) ->
          bind:('b_acc -> t_ Var.t -> 'b_acc * t_ Var.t) ->
          'b_acc -> t_ -> t_
        val map_pol :
          f:('b_acc -> Polarity.t -> t_ -> t_) ->
          bind:('b_acc -> t_ Var.t -> 'b_acc * t_ Var.t) ->
          'b_acc -> Polarity.t -> t_ -> t_
        val approx_infinite_quant_pol :
          [ `Eq | `Exists | `Forall ] ->
          Polarity.t -> [ `Keep | `Unsat_means_unknown of t_ ]
        val size : t_ -> int
        type subst = (t_, t_) Var.Subst.t
        type renaming = (t_, t_ Var.t) Var.Subst.t
        val equal_with : subst:subst -> t_ -> t_ -> bool
        val deref : subst:subst -> t_ -> t_
        val rename_var : subst -> t_ Var.t -> subst * t_ Var.t
        type apply_error =
          TermInner.Util(T).apply_error = {
          ae_msg : string;
          ae_term : t_ option;
          ae_ty : t_;
          ae_args : t_ list;
          ae_args_ty : t_ list;
          ae_subst : subst;
        }
        exception ApplyError of apply_error
        val eval : ?rec_:bool -> subst:subst -> t_ -> t_
        val eval_renaming : subst:renaming -> t_ -> t_
        val renaming_to_subst : renaming -> subst
        val ty_apply : t_ -> terms:t_ list -> tys:t_ list -> t_
        val ty_apply_full : t_ -> terms:t_ list -> tys:t_ list -> t_ * subst
        val ty_apply_mono : t_ -> tys:t_ list -> t_
        type signature = TI.id -> t_ option
        val ty : sigma:signature -> t_ -> t_ TI.or_error
        val ty_exn : sigma:signature -> t_ -> t_
        exception UnifError of string * t_ * t_
        val match_exn : ?subst2:subst -> t_ -> t_ -> subst
        val match_ : ?subst2:subst -> t_ -> t_ -> subst option
      end
    type t = T.t
    val convert_ty : FO.Ty.t -> TermMono.OfFO.U.t_
    val convert_top_ty : FO.Ty.t list * FO.Ty.t -> T.t
    val convert_term : FO.T.t -> TermMono.OfFO.U.t_
    val convert_model :
      (FO.T.t, FO.Ty.t) Model.t ->
      (TermMono.OfFO.U.t_, TermMono.OfFO.U.t_) Model.t
  end