sig
  module QED :
    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 bind
      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 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, bind, 'a) Qed.Logic.term_repr
      type repr = term expression
      type path = int list
      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
      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 : 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 : Qed.Logic.binder -> var -> term -> term
      val e_apply : term -> term list -> term
      type sigma
      val sigma : unit -> sigma
      val sigma_add : sigma -> term Tmap.t -> unit
      val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
      val e_subst_var : var -> term -> term -> term
      val lc_bind : var -> term -> bind
      val lc_open : var -> bind -> term
      val lc_open_term : term -> bind -> term
      val lc_closed : term -> bool
      val lc_closed_at : int -> term -> bool
      val lc_vars : term -> Qed.Bvars.t
      val lc_repr : bind -> term
      val binders : term -> Qed.Logic.binder list
      val e_map : pool -> (term -> term) -> term -> term
      val e_iter : pool -> (term -> unit) -> term -> unit
      val f_map : (int -> term -> term) -> int -> term -> term
      val f_iter : (int -> term -> unit) -> int -> term -> unit
      val lc_map : (term -> term) -> term -> term
      val lc_iter : (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 : Fun.t -> (term list -> term) -> unit
      val set_builtin_map : Fun.t -> (term list -> term list) -> unit
      val set_builtin_get : Fun.t -> (term list -> term -> term) -> unit
      val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
      val set_builtin_leq : 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
  type var = Wp.Lang.F.QED.var
  type tau = Wp.Lang.F.QED.tau
  type pool = Wp.Lang.F.QED.pool
  module Tau = QED.Tau
  module Var = QED.Var
  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
  val pool : ?copy:Wp.Lang.F.pool -> unit -> Wp.Lang.F.pool
  val fresh :
    Wp.Lang.F.pool -> ?basename:string -> Wp.Lang.F.tau -> Wp.Lang.F.var
  val add_var : Wp.Lang.F.pool -> Wp.Lang.F.var -> unit
  val add_vars : Wp.Lang.F.pool -> Wp.Lang.F.Vars.t -> unit
  val tau_of_var : Wp.Lang.F.var -> Wp.Lang.F.tau
  type term = Wp.Lang.F.QED.term
  type record = (Wp.Lang.field * Wp.Lang.F.term) list
  val hash : Wp.Lang.F.term -> int
  val equal : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
  val compare : Wp.Lang.F.term -> Wp.Lang.F.term -> int
  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
  type unop = Wp.Lang.F.term -> Wp.Lang.F.term
  type binop = Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_zero : Wp.Lang.F.term
  val e_one : Wp.Lang.F.term
  val e_minus_one : Wp.Lang.F.term
  val e_minus_one_real : Wp.Lang.F.term
  val e_one_real : Wp.Lang.F.term
  val e_zero_real : Wp.Lang.F.term
  val constant : Wp.Lang.F.term -> Wp.Lang.F.term
  val e_fact : int -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_int64 : int64 -> Wp.Lang.F.term
  val e_bigint : Integer.t -> Wp.Lang.F.term
  val e_float : float -> Wp.Lang.F.term
  val e_setfield :
    Wp.Lang.F.term -> Wp.Lang.field -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_range : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val is_zero : Wp.Lang.F.term -> bool
  val e_true : Wp.Lang.F.term
  val e_false : Wp.Lang.F.term
  val e_bool : bool -> Wp.Lang.F.term
  val e_literal : bool -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_int : int -> Wp.Lang.F.term
  val e_zint : Z.t -> Wp.Lang.F.term
  val e_real : Q.t -> Wp.Lang.F.term
  val e_var : Wp.Lang.F.var -> Wp.Lang.F.term
  val e_opp : Wp.Lang.F.term -> Wp.Lang.F.term
  val e_times : Z.t -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_sum : Wp.Lang.F.term list -> Wp.Lang.F.term
  val e_prod : Wp.Lang.F.term list -> Wp.Lang.F.term
  val e_add : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_sub : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_mul : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_div : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_mod : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_eq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_neq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_leq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_lt : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_imply : Wp.Lang.F.term list -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_equiv : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_and : Wp.Lang.F.term list -> Wp.Lang.F.term
  val e_or : Wp.Lang.F.term list -> Wp.Lang.F.term
  val e_not : Wp.Lang.F.term -> Wp.Lang.F.term
  val e_if :
    Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_const : Wp.Lang.F.tau -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_get : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_set :
    Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
  val e_getfield : Wp.Lang.F.term -> Wp.Lang.Field.t -> Wp.Lang.F.term
  val e_record : Wp.Lang.F.record -> Wp.Lang.F.term
  val e_fun : Wp.Lang.Fun.t -> Wp.Lang.F.term list -> Wp.Lang.F.term
  val e_bind :
    Qed.Logic.binder -> Wp.Lang.F.var -> Wp.Lang.F.term -> Wp.Lang.F.term
  type pred
  type cmp = Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
  type operator = Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  module Pmap :
    sig
      type key = pred
      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 Pset :
    sig
      type elt = pred
      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
  val p_true : Wp.Lang.F.pred
  val p_false : Wp.Lang.F.pred
  val p_equal : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
  val p_equals :
    (Wp.Lang.F.term * Wp.Lang.F.term) list -> Wp.Lang.F.pred list
  val p_neq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
  val p_leq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
  val p_lt : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
  val p_positive : Wp.Lang.F.term -> Wp.Lang.F.pred
  val is_ptrue : Wp.Lang.F.pred -> Qed.Logic.maybe
  val is_pfalse : Wp.Lang.F.pred -> Qed.Logic.maybe
  val is_equal : Wp.Lang.F.term -> Wp.Lang.F.term -> Qed.Logic.maybe
  val eqp : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool
  val comparep : Wp.Lang.F.pred -> Wp.Lang.F.pred -> int
  val p_bool : Wp.Lang.F.term -> Wp.Lang.F.pred
  val e_prop : Wp.Lang.F.pred -> Wp.Lang.F.term
  val p_bools : Wp.Lang.F.term list -> Wp.Lang.F.pred list
  val e_props : Wp.Lang.F.pred list -> Wp.Lang.F.term list
  val lift :
    (Wp.Lang.F.term -> Wp.Lang.F.term) -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_not : Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_and : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_or : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_imply : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_equiv : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_hyps : Wp.Lang.F.pred list -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_if :
    Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_conj : Wp.Lang.F.pred list -> Wp.Lang.F.pred
  val p_disj : Wp.Lang.F.pred list -> Wp.Lang.F.pred
  val p_any : ('-> Wp.Lang.F.pred) -> 'a list -> Wp.Lang.F.pred
  val p_all : ('-> Wp.Lang.F.pred) -> 'a list -> Wp.Lang.F.pred
  val p_call : Wp.Lang.lfun -> Wp.Lang.F.term list -> Wp.Lang.F.pred
  val p_forall : Wp.Lang.F.var list -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_exists : Wp.Lang.F.var list -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_bind :
    Qed.Logic.binder -> Wp.Lang.F.var -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  type sigma = Wp.Lang.F.QED.sigma
  val sigma : unit -> Wp.Lang.F.sigma
  val e_subst :
    ?sigma:Wp.Lang.F.sigma ->
    (Wp.Lang.F.term -> Wp.Lang.F.term) -> Wp.Lang.F.term -> Wp.Lang.F.term
  val p_subst :
    ?sigma:Wp.Lang.F.sigma ->
    (Wp.Lang.F.term -> Wp.Lang.F.term) -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val p_apply :
    Wp.Lang.F.var -> Wp.Lang.F.term -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  val e_vars : Wp.Lang.F.term -> Wp.Lang.F.var list
  val p_vars : Wp.Lang.F.pred -> Wp.Lang.F.var list
  val p_close : Wp.Lang.F.pred -> Wp.Lang.F.pred
  val pp_tau : Stdlib.Format.formatter -> Wp.Lang.F.tau -> unit
  val pp_var : Stdlib.Format.formatter -> Wp.Lang.F.var -> unit
  val pp_vars : Stdlib.Format.formatter -> Wp.Lang.F.Vars.t -> unit
  val pp_term : Stdlib.Format.formatter -> Wp.Lang.F.term -> unit
  val pp_pred : Stdlib.Format.formatter -> Wp.Lang.F.pred -> unit
  val debugp : Stdlib.Format.formatter -> Wp.Lang.F.pred -> unit
  type env
  val context_pp : Wp.Lang.F.env Wp.Context.value
  type marks = Wp.Lang.F.QED.marks
  val env : Wp.Lang.F.Vars.t -> Wp.Lang.F.env
  val marker : Wp.Lang.F.env -> Wp.Lang.F.marks
  val mark_e : Wp.Lang.F.marks -> Wp.Lang.F.term -> unit
  val mark_p : Wp.Lang.F.marks -> Wp.Lang.F.pred -> unit
  val defs : Wp.Lang.F.marks -> Wp.Lang.F.term list
  val define :
    (Wp.Lang.F.env -> string -> Wp.Lang.F.term -> unit) ->
    Wp.Lang.F.env -> Wp.Lang.F.marks -> Wp.Lang.F.env
  val pp_eterm :
    Wp.Lang.F.env -> Stdlib.Format.formatter -> Wp.Lang.F.term -> unit
  val pp_epred :
    Wp.Lang.F.env -> Stdlib.Format.formatter -> Wp.Lang.F.pred -> unit
  val p_expr : Wp.Lang.F.pred -> Wp.Lang.F.pred Wp.Lang.F.QED.expression
  val e_expr : Wp.Lang.F.pred -> Wp.Lang.F.term Wp.Lang.F.QED.expression
  val p_iter :
    (Wp.Lang.F.pred -> unit) ->
    (Wp.Lang.F.term -> unit) -> Wp.Lang.F.pred -> unit
  val lc_closed : Wp.Lang.F.term -> bool
  val lc_iter : (Wp.Lang.F.term -> unit) -> Wp.Lang.F.term -> unit
  val lc_map :
    (Wp.Lang.F.term -> Wp.Lang.F.term) -> Wp.Lang.F.term -> Wp.Lang.F.term
  val decide : Wp.Lang.F.term -> bool
  val basename : Wp.Lang.F.term -> string
  val is_true : Wp.Lang.F.term -> Qed.Logic.maybe
  val is_false : Wp.Lang.F.term -> Qed.Logic.maybe
  val is_prop : Wp.Lang.F.term -> bool
  val is_int : Wp.Lang.F.term -> bool
  val is_real : Wp.Lang.F.term -> bool
  val is_arith : Wp.Lang.F.term -> bool
  val is_closed : Wp.Lang.F.term -> bool
  val is_simple : Wp.Lang.F.term -> bool
  val is_atomic : Wp.Lang.F.term -> bool
  val is_primitive : Wp.Lang.F.term -> bool
  val is_neutral : Wp.Lang.Fun.t -> Wp.Lang.F.term -> bool
  val is_absorbant : Wp.Lang.Fun.t -> Wp.Lang.F.term -> bool
  val record_with :
    Wp.Lang.F.record -> (Wp.Lang.F.term * Wp.Lang.F.record) option
  val are_equal : Wp.Lang.F.term -> Wp.Lang.F.term -> Qed.Logic.maybe
  val eval_eq : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
  val eval_neq : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
  val eval_lt : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
  val eval_leq : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
  val repr : Wp.Lang.F.term -> Wp.Lang.F.QED.repr
  val sort : Wp.Lang.F.term -> Qed.Logic.sort
  val vars : Wp.Lang.F.term -> Wp.Lang.F.Vars.t
  val varsp : Wp.Lang.F.pred -> Wp.Lang.F.Vars.t
  val occurs : Wp.Lang.F.var -> Wp.Lang.F.term -> bool
  val occursp : Wp.Lang.F.var -> Wp.Lang.F.pred -> bool
  val intersect : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
  val intersectp : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool
  val is_subterm : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
  val typeof :
    ?field:(Wp.Lang.Field.t -> Wp.Lang.F.tau) ->
    ?record:(Wp.Lang.Field.t -> Wp.Lang.F.tau) ->
    ?call:(Wp.Lang.Fun.t -> Wp.Lang.F.tau option list -> Wp.Lang.F.tau) ->
    Wp.Lang.F.term -> Wp.Lang.F.tau
  val set_builtin :
    Wp.Lang.lfun -> (Wp.Lang.F.term list -> Wp.Lang.F.term) -> unit
  val set_builtin_get :
    Wp.Lang.lfun ->
    (Wp.Lang.F.term list -> Wp.Lang.F.term -> Wp.Lang.F.term) -> unit
  val set_builtin_1 : Wp.Lang.lfun -> Wp.Lang.F.unop -> unit
  val set_builtin_2 : Wp.Lang.lfun -> Wp.Lang.F.binop -> unit
  val set_builtin_eq : Wp.Lang.lfun -> Wp.Lang.F.binop -> unit
  val set_builtin_leq : Wp.Lang.lfun -> Wp.Lang.F.binop -> unit
  val set_builtin_eqp : Wp.Lang.lfun -> Wp.Lang.F.cmp -> unit
  val release : unit -> unit
  module Check :
    sig
      val reset : unit -> unit
      val set : string -> unit
      val is_set : unit -> bool
      val iter :
        (qed:Wp.Lang.F.term ->
         raw:Wp.Lang.F.term -> goal:Wp.Lang.F.pred -> unit) ->
        unit
    end
end