sig
  module ADT :
    sig
      type t = adt
      val hash : t -> int
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val pretty : Format.formatter -> t -> unit
      val debug : t -> string
      val basename : t -> string
    end
  module Field :
    sig
      type t = field
      val hash : t -> int
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val pretty : Format.formatter -> t -> unit
      val debug : t -> string
      val sort : t -> Qed.Logic.sort
    end
  module Fun :
    sig
      type t = lfun
      val hash : t -> int
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val pretty : Format.formatter -> t -> unit
      val debug : t -> string
      val category : t -> t Qed.Logic.category
      val params : t -> Qed.Logic.sort list
      val sort : t -> Qed.Logic.sort
    end
  module Var : Qed.Logic.Variable
  type term
  type lc_term
  module Term :
    sig
      type t = term
      val hash : t -> int
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val pretty : Format.formatter -> t -> unit
      val debug : t -> string
    end
  module Tset :
    sig
      type elt = term
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val find : elt -> t -> elt
      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) -> 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 map : (elt -> elt) -> t -> t
      val mapf : (elt -> elt option) -> t -> t
      val intersect : t -> t -> bool
    end
  module Tmap :
    sig
      type key = term
      type 'a t
      val is_empty : 'a t -> bool
      val empty : 'a t
      val add : key -> '-> 'a t -> 'a t
      val mem : key -> 'a t -> bool
      val find : key -> 'a t -> 'a
      val remove : key -> '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 map : (key -> '-> 'b) -> 'a t -> 'b t
      val mapf : (key -> '-> 'b option) -> 'a t -> 'b t
      val mapq : (key -> '-> 'a option) -> 'a t -> 'a t
      val filter : (key -> '-> bool) -> 'a t -> 'a t
      val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t
      val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t
      val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
      val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
      val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val iter2 :
        (key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
      val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
      val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
      val change :
        (key -> '-> 'a option -> 'a option) -> key -> '-> 'a t -> 'a t
    end
  module STset :
    sig
      type elt = term
      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 disjoint : t -> t -> bool
      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 map : (elt -> elt) -> t -> t
      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 min_elt_opt : t -> elt option
      val max_elt : t -> elt
      val max_elt_opt : t -> elt option
      val choose : t -> elt
      val choose_opt : t -> elt option
      val split : elt -> t -> t * bool * t
      val find : elt -> t -> elt
      val find_opt : elt -> t -> elt option
      val find_first : (elt -> bool) -> t -> elt
      val find_first_opt : (elt -> bool) -> t -> elt option
      val find_last : (elt -> bool) -> t -> elt
      val find_last_opt : (elt -> bool) -> t -> elt option
      val of_list : elt list -> t
      val to_seq_from : elt -> t -> elt Seq.t
      val to_seq : t -> elt Seq.t
      val add_seq : elt Seq.t -> t -> t
      val of_seq : elt Seq.t -> t
    end
  module STmap :
    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 update : key -> ('a option -> 'a option) -> '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 min_binding_opt : 'a t -> (key * 'a) option
      val max_binding : 'a t -> key * 'a
      val max_binding_opt : 'a t -> (key * 'a) option
      val choose : 'a t -> key * 'a
      val choose_opt : 'a t -> (key * 'a) option
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_first : (key -> bool) -> 'a t -> key * 'a
      val find_first_opt : (key -> bool) -> 'a t -> (key * 'a) option
      val find_last : (key -> bool) -> 'a t -> key * 'a
      val find_last_opt : (key -> bool) -> 'a t -> (key * 'a) option
      val map : ('-> 'b) -> 'a t -> 'b t
      val mapi : (key -> '-> 'b) -> 'a t -> 'b t
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
      val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
      val of_seq : (key * 'a) Seq.t -> 'a t
    end
  type var = Var.t
  type tau = (Field.t, ADT.t) Qed.Logic.datatype
  module Tau :
    sig
      type t = tau
      val hash : t -> int
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val pretty : Format.formatter -> t -> unit
      val debug : t -> string
      val basename : t -> string
    end
  module Vars :
    sig
      type elt = var
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val find : elt -> t -> elt
      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) -> 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 map : (elt -> elt) -> t -> t
      val mapf : (elt -> elt option) -> t -> t
      val intersect : t -> t -> bool
    end
  module Vmap :
    sig
      type key = var
      type 'a t
      val is_empty : 'a t -> bool
      val empty : 'a t
      val add : key -> '-> 'a t -> 'a t
      val mem : key -> 'a t -> bool
      val find : key -> 'a t -> 'a
      val remove : key -> '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 map : (key -> '-> 'b) -> 'a t -> 'b t
      val mapf : (key -> '-> 'b option) -> 'a t -> 'b t
      val mapq : (key -> '-> 'a option) -> 'a t -> 'a t
      val filter : (key -> '-> bool) -> 'a t -> 'a t
      val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t
      val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t
      val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
      val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
      val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val iter2 :
        (key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
      val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
      val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
      val change :
        (key -> '-> 'a option -> 'a option) -> key -> '-> 'a t -> 'a t
    end
  type pool
  val pool : ?copy:pool -> unit -> pool
  val add_var : pool -> var -> unit
  val add_vars : pool -> Vars.t -> unit
  val add_term : pool -> term -> unit
  val fresh : pool -> ?basename:string -> tau -> var
  val alpha : pool -> var -> var
  val tau_of_var : var -> tau
  val sort_of_var : var -> Qed.Logic.sort
  val base_of_var : var -> string
  type 'a expression =
      (Field.t, ADT.t, Fun.t, var, lc_term, 'a) Qed.Logic.term_repr
  type repr = term expression
  type record = (Field.t * term) list
  val decide : term -> bool
  val is_true : term -> Qed.Logic.maybe
  val is_false : term -> Qed.Logic.maybe
  val is_prop : term -> bool
  val is_int : term -> bool
  val is_real : term -> bool
  val is_arith : term -> bool
  val are_equal : term -> term -> Qed.Logic.maybe
  val eval_eq : term -> term -> bool
  val eval_neq : term -> term -> bool
  val eval_lt : term -> term -> bool
  val eval_leq : term -> term -> bool
  val repr : term -> repr
  val sort : term -> Qed.Logic.sort
  val vars : term -> Vars.t
  type path = int list
  val subterm : term -> path -> term
  val change_subterm : term -> path -> term -> term
  val e_true : term
  val e_false : term
  val e_bool : bool -> term
  val e_literal : bool -> term -> term
  val e_int : int -> term
  val e_float : float -> term
  val e_zint : Z.t -> term
  val e_real : Q.t -> term
  val e_var : var -> term
  val e_opp : term -> term
  val e_times : Z.t -> term -> term
  val e_sum : term list -> term
  val e_prod : term list -> term
  val e_add : term -> term -> term
  val e_sub : term -> term -> term
  val e_mul : term -> term -> term
  val e_div : term -> term -> term
  val e_mod : term -> term -> term
  val e_eq : term -> term -> term
  val e_neq : term -> term -> term
  val e_leq : term -> term -> term
  val e_lt : term -> term -> term
  val e_imply : term list -> term -> term
  val e_equiv : term -> term -> term
  val e_and : term list -> term
  val e_or : term list -> term
  val e_not : term -> term
  val e_if : term -> term -> term -> term
  val e_const : tau -> term -> term
  val e_get : term -> term -> term
  val e_set : term -> term -> term -> term
  val e_getfield : term -> Field.t -> term
  val e_record : record -> term
  val e_fun : ?result:tau -> Fun.t -> term list -> term
  val e_repr : ?result:tau -> repr -> term
  val e_forall : var list -> term -> term
  val e_exists : var list -> term -> term
  val e_lambda : var list -> term -> term
  val e_apply : term -> term list -> term
  val e_bind : Qed.Logic.binder -> var -> term -> term
  val lc_open : var -> lc_term -> term
  val e_unbind : var -> lc_term -> term
  val e_open :
    pool:pool ->
    ?forall:bool ->
    ?exists:bool ->
    ?lambda:bool -> term -> (Qed.Logic.binder * var) list * term
  val e_close : (Qed.Logic.binder * var) list -> term -> term
  type sigma
  val sigma : ?pool:pool -> unit -> sigma
  module Subst :
    sig
      type t = sigma
      val create : ?pool:pool -> unit -> t
      val fresh : t -> tau -> var
      val get : t -> term -> term
      val filter : t -> term -> bool
      val add : t -> term -> term -> unit
      val add_map : t -> term Tmap.t -> unit
      val add_fun : t -> (term -> term) -> unit
      val add_filter : t -> (term -> bool) -> unit
      val add_var : t -> var -> unit
      val add_vars : t -> Vars.t -> unit
      val add_term : t -> term -> unit
    end
  val e_subst : sigma -> term -> term
  val e_subst_var : var -> term -> term -> term
  val lc_vars : term -> Qed.Bvars.t
  val lc_closed : term -> bool
  val lc_repr : lc_term -> term
  val lc_iter : (term -> unit) -> term -> unit
  val f_map :
    ?pool:pool ->
    ?forall:bool ->
    ?exists:bool -> ?lambda:bool -> (term -> term) -> term -> term
  val f_iter :
    ?pool:pool ->
    ?forall:bool ->
    ?exists:bool -> ?lambda:bool -> (term -> unit) -> term -> unit
  val typeof :
    ?field:(Field.t -> tau) ->
    ?record:(Field.t -> tau) ->
    ?call:(Fun.t -> tau option list -> tau) -> term -> tau
  val set_builtin : ?force:bool -> Fun.t -> (term list -> term) -> unit
  val set_builtin' :
    ?force:bool -> Fun.t -> (term list -> tau option -> term) -> unit
  val set_builtin_map :
    ?force:bool -> Fun.t -> (term list -> term list) -> unit
  val set_builtin_get :
    ?force:bool -> Fun.t -> (term list -> tau option -> term -> term) -> unit
  val set_builtin_eq : ?force:bool -> Fun.t -> (term -> term -> term) -> unit
  val set_builtin_leq :
    ?force:bool -> Fun.t -> (term -> term -> term) -> unit
  val consequence : term -> term -> term
  val literal : term -> bool * term
  val affine : term -> term Qed.Logic.affine
  val record_with : record -> (term * record) option
  type t = term
  val id : t -> int
  val hash : t -> int
  val equal : t -> t -> bool
  val compare : t -> t -> int
  val pretty : Format.formatter -> t -> unit
  val weigth : t -> int
  val is_closed : t -> bool
  val is_simple : t -> bool
  val is_atomic : t -> bool
  val is_primitive : t -> bool
  val is_neutral : Fun.t -> t -> bool
  val is_absorbant : Fun.t -> t -> bool
  val size : t -> int
  val basename : t -> string
  val debug : Format.formatter -> t -> unit
  val pp_id : Format.formatter -> t -> unit
  val pp_rid : Format.formatter -> t -> unit
  val pp_repr : Format.formatter -> repr -> unit
  val is_subterm : term -> term -> bool
  val shared :
    ?shared:(term -> bool) ->
    ?shareable:(term -> bool) ->
    ?subterms:((term -> unit) -> term -> unit) -> term list -> term list
  type marks
  val marks :
    ?shared:(term -> bool) ->
    ?shareable:(term -> bool) ->
    ?subterms:((term -> unit) -> term -> unit) -> unit -> marks
  val mark : marks -> term -> unit
  val share : marks -> term -> unit
  val defs : marks -> term list
end