sig
  type t_
  val head_sym : TermInner.UTIL_REPR.t_ -> TermInner.id
  val to_seq : TermInner.UTIL_REPR.t_ -> TermInner.UTIL_REPR.t_ Sequence.t
  val to_seq_vars :
    TermInner.UTIL_REPR.t_ -> TermInner.UTIL_REPR.t_ Var.t Sequence.t
  val to_seq_consts : TermInner.UTIL_REPR.t_ -> ID.t Sequence.t
  module VarSet :
    sig
      type elt = t_ Var.t
      type 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:TermInner.UTIL_REPR.VarSet.t ->
    TermInner.UTIL_REPR.t_ -> TermInner.UTIL_REPR.t_ Var.t Sequence.t
  val free_vars :
    ?bound:TermInner.UTIL_REPR.VarSet.t ->
    TermInner.UTIL_REPR.t_ -> TermInner.UTIL_REPR.VarSet.t
  val is_var : TermInner.UTIL_REPR.t_ -> bool
  val is_const : TermInner.UTIL_REPR.t_ -> bool
  val is_closed : TermInner.UTIL_REPR.t_ -> bool
  val is_undefined : TermInner.UTIL_REPR.t_ -> bool
  val free_meta_vars :
    ?init:TermInner.UTIL_REPR.t_ MetaVar.t ID.Map.t ->
    TermInner.UTIL_REPR.t_ -> TermInner.UTIL_REPR.t_ MetaVar.t ID.Map.t
  val bind_unfold :
    TermInner.Binder.t ->
    TermInner.UTIL_REPR.t_ ->
    TermInner.UTIL_REPR.t_ Var.t list * TermInner.UTIL_REPR.t_
  val fun_unfold :
    TermInner.UTIL_REPR.t_ ->
    TermInner.UTIL_REPR.t_ Var.t list * TermInner.UTIL_REPR.t_
  val get_ty_arg :
    TermInner.UTIL_REPR.t_ -> int -> TermInner.UTIL_REPR.t_ option
  val ty_unfold :
    TermInner.UTIL_REPR.t_ ->
    TermInner.UTIL_REPR.t_ Var.t list * TermInner.UTIL_REPR.t_ list *
    TermInner.UTIL_REPR.t_
  val ty_is_Type : TermInner.UTIL_REPR.t_ -> bool
  val ty_returns_Type : TermInner.UTIL_REPR.t_ -> bool
  val ty_returns_Prop : TermInner.UTIL_REPR.t_ -> bool
  val ty_returns : TermInner.UTIL_REPR.t_ -> TermInner.UTIL_REPR.t_
  val ty_is_Kind : TermInner.UTIL_REPR.t_ -> bool
  val ty_is_Prop : TermInner.UTIL_REPR.t_ -> bool
  val ty_is_unitype : TermInner.UTIL_REPR.t_ -> bool
  val ty_num_param : TermInner.UTIL_REPR.t_ -> int
end