sig
  type 'a element =
    'Qed.Logic.element =
      E_none
    | E_true
    | E_false
    | E_int of int
    | E_const of 'a
  type 'a operator =
    'Qed.Logic.operator = {
    inversible : bool;
    associative : bool;
    commutative : bool;
    idempotent : bool;
    neutral : 'a element;
    absorbant : 'a element;
  }
  type 'a category =
    'Qed.Logic.category =
      Function
    | Constructor
    | Injection
    | Operator of 'a operator
  type binder = Qed.Logic.binder = Forall | Exists | Lambda
  type ('f, 'a) datatype =
    ('f, 'a) Qed.Logic.datatype =
      Prop
    | Bool
    | Int
    | Real
    | Tvar of int
    | Array of ('f, 'a) datatype * ('f, 'a) datatype
    | Record of ('f * ('f, 'a) datatype) list
    | Data of 'a * ('f, 'a) datatype list
  type sort =
    Qed.Logic.sort =
      Sprop
    | Sbool
    | Sint
    | Sreal
    | Sdata
    | Sarray of sort
  type maybe = Qed.Logic.maybe = Yes | No | Maybe
  module type Symbol =
    sig
      type t
      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 type Data =
    sig
      type t
      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 type Field =
    sig
      type t
      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 -> sort
    end
  module type Function =
    sig
      type t
      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 category
      val params : t -> sort list
      val sort : t -> sort
    end
  module type Variable =
    sig
      type t
      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 -> sort
      val basename : t -> string
      val dummy : t
    end
  type ('f, 'a) funtype =
    ('f, 'a) Qed.Logic.funtype = {
    result : ('f, 'a) datatype;
    params : ('f, 'a) datatype list;
  }
  type ('z, 'f, 'd, 'x, 'e) term_repr =
    ('z, 'f, 'd, 'x, 'e) Qed.Logic.term_repr =
      True
    | False
    | Kint of 'z
    | Kreal of Qed.R.t
    | Times of 'z * 'e
    | Add of 'e list
    | Mul of 'e list
    | Div of 'e * 'e
    | Mod of 'e * 'e
    | Eq of 'e * 'e
    | Neq of 'e * 'e
    | Leq of 'e * 'e
    | Lt of 'e * 'e
    | Aget of 'e * 'e
    | Aset of 'e * 'e * 'e
    | Rget of 'e * 'f
    | Rdef of ('f * 'e) list
    | And of 'e list
    | Or of 'e list
    | Not of 'e
    | Imply of 'e list * 'e
    | If of 'e * 'e * 'e
    | Fun of 'd * 'e list
    | Var of 'x
    | Apply of 'e * 'e list
    | Bind of binder * 'x * 'e
  type ('z, 'a) affine =
    ('z, 'a) Qed.Logic.affine = {
    constant : 'z;
    factors : ('z * 'a) list;
  }
  module type Term =
    sig
      module Z : Qed.Arith.Z
      module ADT : Data
      module Field : Field
      module Fun : Function
      module Var : Variable
      type term
      type var = Var.t
      type tau = (Field.t, ADT.t) datatype
      type signature = (Field.t, ADT.t) funtype
      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 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 base_of_var : var -> string
      type 'a expression = (Z.t, Field.t, Fun.t, var, 'a) term_repr
      type repr = term expression
      type path = int list
      type record = (Field.t * term) list
      val decide : term -> bool
      val is_true : term -> maybe
      val is_false : term -> 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 -> 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 -> sort
      val vars : term -> Vars.t
      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_zint : Z.t -> term
      val e_real : Qed.R.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_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 : Fun.t -> term list -> term
      val e_repr : 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_bind : binder -> var -> term -> term
      val e_subst : ?pool:pool -> var -> term -> term -> term
      val e_apply : ?pool:pool -> term -> term list -> term
      val r_map : ('-> term) -> 'a expression -> term
      val e_map : (term -> term) -> term -> term
      val e_iter : (term -> unit) -> term -> unit
      val f_map : (Vars.t -> term -> term) -> Vars.t -> term -> term
      val f_iter : (Vars.t -> term -> unit) -> Vars.t -> term -> unit
      val set_builtin : Fun.t -> (term list -> term) -> unit
      val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
      val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit
      val literal : term -> bool * term
      val congruence_eq : term -> term -> (term * term) list option
      val congruence_neq : term -> term -> (term * term) list option
      val flattenable : term -> bool
      val flattens : term -> term -> bool
      val flatten : term -> term list
      val affine : term -> (Z.t, term) 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
      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 insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
          val change :
            (key -> '-> 'a option -> 'a option) ->
            key -> '-> 'a t -> 'a t
        end
      val shared :
        ?shared:(term -> bool) ->
        ?shareable:(term -> bool) -> ?closed:Vars.t -> term list -> term list
      type marks
      val marks :
        ?shared:(term -> bool) ->
        ?shareable:(term -> bool) -> ?closed:Vars.t -> unit -> marks
      val mark : marks -> term -> unit
      val defs : marks -> term list
    end
end