From de9c46d059ddd38c0c1922d91cb788c3d550d488 Mon Sep 17 00:00:00 2001
From: ckeller <ckeller@users.noreply.github.com>
Date: Sat, 30 Jul 2022 16:42:50 +0200
Subject: Extraction for Coq 8.13 (#109)

Extraction is back! Some new features:
* Not only an executable is generated, but the ZChaff and veriT checkers are available through a package called Smtcoq_extr
* The command-line arguments are better handled
* The veriT checker is now the default
---
 src/extraction/sat_checker.ml | 2726 ++++++++++++++++++++++++++++++++++++-----
 1 file changed, 2414 insertions(+), 312 deletions(-)

(limited to 'src/extraction/sat_checker.ml')

diff --git a/src/extraction/sat_checker.ml b/src/extraction/sat_checker.ml
index 839f95b..9d881f4 100644
--- a/src/extraction/sat_checker.ml
+++ b/src/extraction/sat_checker.ml
@@ -1,14 +1,6 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2022                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
 
+type __ = Obj.t
+let __ = let rec f _ = Obj.repr f in Obj.repr f
 
 (** val negb : bool -> bool **)
 
@@ -16,232 +8,2400 @@ let negb = function
 | true -> false
 | false -> true
 
+type nat =
+| O
+| S of nat
+
+type 'a option =
+| Some of 'a
+| None
+
+(** val fst : ('a1 * 'a2) -> 'a1 **)
+
+let fst = function
+| (x, _) -> x
+
+(** val snd : ('a1 * 'a2) -> 'a2 **)
+
+let snd = function
+| (_, y) -> y
+
 type 'a list =
 | Nil
 | Cons of 'a * 'a list
 
-(** val existsb : ('a1 -> bool) -> 'a1 list -> bool **)
+(** val app : 'a1 list -> 'a1 list -> 'a1 list **)
+
+let rec app l m =
+  match l with
+  | Nil -> m
+  | Cons (a, l1) -> Cons (a, (app l1 m))
+
+(** val compOpp : int -> int **)
+
+let compOpp = function
+| 0 -> 0
+| (-1) -> 1
+| 1 -> (-1)
+
+type sumbool =
+| Left
+| Right
+
+(** val add : nat -> nat -> nat **)
+
+let rec add n m =
+  match n with
+  | O -> m
+  | S p -> S (add p m)
+
+type positive =
+| XI of positive
+| XO of positive
+| XH
+
+type z =
+| Z0
+| Zpos of positive
+| Zneg of positive
+
+module type EqLtLe =
+ sig
+  type t
+ end
+
+module MakeOrderTac =
+ functor (O:EqLtLe) ->
+ functor (P:sig
+ end) ->
+ struct
+ end
+
+module Pos =
+ struct
+  (** val succ : positive -> positive **)
+
+  let rec succ = function
+  | XI p -> XO (succ p)
+  | XO p -> XI p
+  | XH -> XO XH
+
+  (** val add : positive -> positive -> positive **)
+
+  let rec add x y =
+    match x with
+    | XI p ->
+      (match y with
+       | XI q -> XO (add_carry p q)
+       | XO q -> XI (add p q)
+       | XH -> XO (succ p))
+    | XO p ->
+      (match y with
+       | XI q -> XI (add p q)
+       | XO q -> XO (add p q)
+       | XH -> XI p)
+    | XH -> (match y with
+             | XI q -> XO (succ q)
+             | XO q -> XI q
+             | XH -> XO XH)
+
+  (** val add_carry : positive -> positive -> positive **)
+
+  and add_carry x y =
+    match x with
+    | XI p ->
+      (match y with
+       | XI q -> XI (add_carry p q)
+       | XO q -> XO (add_carry p q)
+       | XH -> XI (succ p))
+    | XO p ->
+      (match y with
+       | XI q -> XO (add_carry p q)
+       | XO q -> XI (add p q)
+       | XH -> XO (succ p))
+    | XH ->
+      (match y with
+       | XI q -> XI (succ q)
+       | XO q -> XO (succ q)
+       | XH -> XI XH)
+
+  (** val pred_double : positive -> positive **)
+
+  let rec pred_double = function
+  | XI p -> XI (XO p)
+  | XO p -> XI (pred_double p)
+  | XH -> XH
+
+  (** val mul : positive -> positive -> positive **)
+
+  let rec mul x y =
+    match x with
+    | XI p -> add y (XO (mul p y))
+    | XO p -> XO (mul p y)
+    | XH -> y
+
+  (** val compare_cont : int -> positive -> positive -> int **)
+
+  let rec compare_cont r x y =
+    match x with
+    | XI p ->
+      (match y with
+       | XI q -> compare_cont r p q
+       | XO q -> compare_cont 1 p q
+       | XH -> 1)
+    | XO p ->
+      (match y with
+       | XI q -> compare_cont (-1) p q
+       | XO q -> compare_cont r p q
+       | XH -> 1)
+    | XH -> (match y with
+             | XH -> r
+             | _ -> (-1))
+
+  (** val compare : positive -> positive -> int **)
+
+  let compare =
+    compare_cont 0
+
+  (** val eqb : positive -> positive -> bool **)
+
+  let rec eqb p q =
+    match p with
+    | XI p0 -> (match q with
+                | XI q0 -> eqb p0 q0
+                | _ -> false)
+    | XO p0 -> (match q with
+                | XO q0 -> eqb p0 q0
+                | _ -> false)
+    | XH -> (match q with
+             | XH -> true
+             | _ -> false)
+
+  (** val eq_dec : positive -> positive -> sumbool **)
+
+  let rec eq_dec p x0 =
+    match p with
+    | XI p0 -> (match x0 with
+                | XI p1 -> eq_dec p0 p1
+                | _ -> Right)
+    | XO p0 -> (match x0 with
+                | XO p1 -> eq_dec p0 p1
+                | _ -> Right)
+    | XH -> (match x0 with
+             | XH -> Left
+             | _ -> Right)
+ end
+
+module Z =
+ struct
+  (** val double : z -> z **)
+
+  let double = function
+  | Z0 -> Z0
+  | Zpos p -> Zpos (XO p)
+  | Zneg p -> Zneg (XO p)
+
+  (** val succ_double : z -> z **)
+
+  let succ_double = function
+  | Z0 -> Zpos XH
+  | Zpos p -> Zpos (XI p)
+  | Zneg p -> Zneg (Pos.pred_double p)
+
+  (** val pred_double : z -> z **)
+
+  let pred_double = function
+  | Z0 -> Zneg XH
+  | Zpos p -> Zpos (Pos.pred_double p)
+  | Zneg p -> Zneg (XI p)
+
+  (** val pos_sub : positive -> positive -> z **)
+
+  let rec pos_sub x y =
+    match x with
+    | XI p ->
+      (match y with
+       | XI q -> double (pos_sub p q)
+       | XO q -> succ_double (pos_sub p q)
+       | XH -> Zpos (XO p))
+    | XO p ->
+      (match y with
+       | XI q -> pred_double (pos_sub p q)
+       | XO q -> double (pos_sub p q)
+       | XH -> Zpos (Pos.pred_double p))
+    | XH ->
+      (match y with
+       | XI q -> Zneg (XO q)
+       | XO q -> Zneg (Pos.pred_double q)
+       | XH -> Z0)
+
+  (** val add : z -> z -> z **)
+
+  let add x y =
+    match x with
+    | Z0 -> y
+    | Zpos x' ->
+      (match y with
+       | Z0 -> x
+       | Zpos y' -> Zpos (Pos.add x' y')
+       | Zneg y' -> pos_sub x' y')
+    | Zneg x' ->
+      (match y with
+       | Z0 -> x
+       | Zpos y' -> pos_sub y' x'
+       | Zneg y' -> Zneg (Pos.add x' y'))
+
+  (** val opp : z -> z **)
+
+  let opp = function
+  | Z0 -> Z0
+  | Zpos x0 -> Zneg x0
+  | Zneg x0 -> Zpos x0
+
+  (** val sub : z -> z -> z **)
+
+  let sub m n =
+    add m (opp n)
+
+  (** val mul : z -> z -> z **)
+
+  let mul x y =
+    match x with
+    | Z0 -> Z0
+    | Zpos x' ->
+      (match y with
+       | Z0 -> Z0
+       | Zpos y' -> Zpos (Pos.mul x' y')
+       | Zneg y' -> Zneg (Pos.mul x' y'))
+    | Zneg x' ->
+      (match y with
+       | Z0 -> Z0
+       | Zpos y' -> Zneg (Pos.mul x' y')
+       | Zneg y' -> Zpos (Pos.mul x' y'))
+
+  (** val compare : z -> z -> int **)
+
+  let compare x y =
+    match x with
+    | Z0 -> (match y with
+             | Z0 -> 0
+             | Zpos _ -> (-1)
+             | Zneg _ -> 1)
+    | Zpos x' -> (match y with
+                  | Zpos y' -> Pos.compare x' y'
+                  | _ -> 1)
+    | Zneg x' ->
+      (match y with
+       | Zneg y' -> compOpp (Pos.compare x' y')
+       | _ -> (-1))
+
+  (** val leb : z -> z -> bool **)
+
+  let leb x y =
+    match compare x y with
+    | 1 -> false
+    | _ -> true
+
+  (** val ltb : z -> z -> bool **)
+
+  let ltb x y =
+    match compare x y with
+    | (-1) -> true
+    | _ -> false
+
+  (** val eqb : z -> z -> bool **)
+
+  let eqb x y =
+    match x with
+    | Z0 -> (match y with
+             | Z0 -> true
+             | _ -> false)
+    | Zpos p -> (match y with
+                 | Zpos q -> Pos.eqb p q
+                 | _ -> false)
+    | Zneg p -> (match y with
+                 | Zneg q -> Pos.eqb p q
+                 | _ -> false)
 
-let rec existsb f = function
-| Nil -> false
-| Cons (a, l0) -> if f a then true else existsb f l0
+  (** val max : z -> z -> z **)
 
-type int = ExtrNative.uint
+  let max n m =
+    match compare n m with
+    | (-1) -> m
+    | _ -> n
 
-(** val lsl0 : int -> int -> int **)
+  (** val eq_dec : z -> z -> sumbool **)
 
-let lsl0 = ExtrNative.l_sl
+  let eq_dec x y =
+    match x with
+    | Z0 -> (match y with
+             | Z0 -> Left
+             | _ -> Right)
+    | Zpos x0 -> (match y with
+                  | Zpos p0 -> Pos.eq_dec x0 p0
+                  | _ -> Right)
+    | Zneg x0 -> (match y with
+                  | Zneg p0 -> Pos.eq_dec x0 p0
+                  | _ -> Right)
+ end
+
+(** val rev : 'a1 list -> 'a1 list **)
+
+let rec rev = function
+| Nil -> Nil
+| Cons (x, l') -> app (rev l') (Cons (x, Nil))
+
+(** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 **)
+
+let rec fold_left f l a0 =
+  match l with
+  | Nil -> a0
+  | Cons (b, t0) -> fold_left f t0 (f a0 b)
+
+(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **)
+
+let rec fold_right f a0 = function
+| Nil -> a0
+| Cons (b, t0) -> f b (fold_right f a0 t0)
+
+(** val size : nat **)
 
-(** val lsr0 : int -> int -> int **)
+let size =
+  S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S
+    (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S
+    (S (S (S (S (S (S (S (S (S (S (S (S (S (S
+    O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
-let lsr0 = ExtrNative.l_sr
+(** val lsl0 : Uint63.t -> Uint63.t -> Uint63.t **)
 
-(** val land0 : int -> int -> int **)
+let lsl0 = Uint63.l_sl
 
-let land0 = ExtrNative.l_and
+(** val lsr0 : Uint63.t -> Uint63.t -> Uint63.t **)
 
-(** val lxor0 : int -> int -> int **)
+let lsr0 = Uint63.l_sr
 
-let lxor0 = ExtrNative.l_xor
+(** val lxor0 : Uint63.t -> Uint63.t -> Uint63.t **)
 
-(** val sub : int -> int -> int **)
+let lxor0 = Uint63.l_xor
 
-let sub = ExtrNative.sub
+(** val add0 : Uint63.t -> Uint63.t -> Uint63.t **)
 
-(** val eqb : int -> int -> bool **)
+let add0 = Uint63.add
 
-let eqb = fun i j -> ExtrNative.compare i j = ExtrNative.Eq
+(** val sub0 : Uint63.t -> Uint63.t -> Uint63.t **)
 
-(** val foldi_cont :
-    (int -> ('a1 -> 'a2) -> 'a1 -> 'a2) -> int -> int -> ('a1 -> 'a2) -> 'a1
-    -> 'a2 **)
+let sub0 = Uint63.sub
 
-let foldi_cont = ExtrNative.foldi_cont
+(** val eqb0 : Uint63.t -> Uint63.t -> bool **)
 
-(** val foldi_down_cont :
-    (int -> ('a1 -> 'a2) -> 'a1 -> 'a2) -> int -> int -> ('a1 -> 'a2) -> 'a1
-    -> 'a2 **)
+let eqb0 = Uint63.equal
 
-let foldi_down_cont = ExtrNative.foldi_down_cont
+(** val ltb0 : Uint63.t -> Uint63.t -> bool **)
 
-(** val is_zero : int -> bool **)
+let ltb0 = Uint63.lt
+
+(** val leb0 : Uint63.t -> Uint63.t -> bool **)
+
+let leb0 = Uint63.le
+
+(** val digits : Uint63.t **)
+
+let digits =
+  (Uint63.of_int (63))
+
+(** val is_zero : Uint63.t -> bool **)
 
 let is_zero i =
-  eqb i (ExtrNative.of_uint(0))
+  eqb0 i (Uint63.of_int (0))
 
-(** val is_even : int -> bool **)
+(** val bit : Uint63.t -> Uint63.t -> bool **)
 
-let is_even i =
-  is_zero (land0 i (ExtrNative.of_uint(1)))
+let bit i n =
+  negb (is_zero (lsl0 (lsr0 i n) (sub0 digits (Uint63.of_int (1)))))
 
-(** val compare : int -> int -> ExtrNative.comparison **)
+(** val compare0 : Uint63.t -> Uint63.t -> int **)
 
-let compare = ExtrNative.compare
+let compare0 = Uint63.compare
 
-(** val foldi : (int -> 'a1 -> 'a1) -> int -> int -> 'a1 -> 'a1 **)
+type 'x compare1 =
+| LT
+| EQ
+| GT
 
-let foldi f from to0 =
-  foldi_cont (fun i cont a -> cont (f i a)) from to0 (fun a -> a)
+module type OrderedType =
+ sig
+  type t
 
-(** val foldi_down : (int -> 'a1 -> 'a1) -> int -> int -> 'a1 -> 'a1 **)
+  val compare : t -> t -> t compare1
 
-let foldi_down f from downto0 =
-  foldi_down_cont (fun i cont a -> cont (f i a)) from downto0 (fun a -> a)
+  val eq_dec : t -> t -> sumbool
+ end
 
-type 'a array = 'a ExtrNative.parray
+module OrderedTypeFacts =
+ functor (O:OrderedType) ->
+ struct
+  module TO =
+   struct
+    type t = O.t
+   end
 
-(** val make : int -> 'a1 -> 'a1 array **)
+  module IsTO =
+   struct
+   end
 
-let make = ExtrNative.parray_make
+  module OrderTac = MakeOrderTac(TO)(IsTO)
 
-module Coq__1 = struct 
- (** val get : 'a1 array -> int -> 'a1 **)
- 
- let get = ExtrNative.parray_get
-end
-let get = Coq__1.get
+  (** val eq_dec : O.t -> O.t -> sumbool **)
 
-(** val set : 'a1 array -> int -> 'a1 -> 'a1 array **)
+  let eq_dec =
+    O.eq_dec
 
-let set = ExtrNative.parray_set
+  (** val lt_dec : O.t -> O.t -> sumbool **)
 
-(** val length : 'a1 array -> int **)
+  let lt_dec x y =
+    match O.compare x y with
+    | LT -> Left
+    | _ -> Right
 
-let length = ExtrNative.parray_length
+  (** val eqb : O.t -> O.t -> bool **)
 
-(** val to_list : 'a1 array -> 'a1 list **)
+  let eqb x y =
+    match eq_dec x y with
+    | Left -> true
+    | Right -> false
+ end
 
-let to_list t0 =
-  let len = length t0 in
-  if eqb (ExtrNative.of_uint(0)) len
-  then Nil
-  else foldi_down (fun i l -> Cons ((get t0 i), l))
-         (sub len (ExtrNative.of_uint(1))) (ExtrNative.of_uint(0)) Nil
+module KeyOrderedType =
+ functor (O:OrderedType) ->
+ struct
+  module MO = OrderedTypeFacts(O)
+ end
 
-(** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 array -> 'a1 **)
+module Raw =
+ functor (X:OrderedType) ->
+ struct
+  module MX = OrderedTypeFacts(X)
 
-let fold_left f a t0 =
-  let len = length t0 in
-  if eqb (ExtrNative.of_uint(0)) len
-  then a
-  else foldi (fun i a0 -> f a0 (get t0 i)) (ExtrNative.of_uint(0))
-         (sub (length t0) (ExtrNative.of_uint(1))) a
-
-(** val foldi_right :
-    (int -> 'a1 -> 'a2 -> 'a2) -> 'a1 array -> 'a2 -> 'a2 **)
-
-let foldi_right f t0 b =
-  let len = length t0 in
-  if eqb (ExtrNative.of_uint(0)) len
-  then b
-  else foldi_down (fun i b0 -> f i (get t0 i) b0)
-         (sub len (ExtrNative.of_uint(1))) (ExtrNative.of_uint(0)) b
-
-module Valuation = 
- struct 
-  type t = int -> bool
+  module PX = KeyOrderedType(X)
+
+  type key = X.t
+
+  type 'elt t = (X.t * 'elt) list
+
+  (** val empty : 'a1 t **)
+
+  let empty =
+    Nil
+
+  (** val is_empty : 'a1 t -> bool **)
+
+  let is_empty = function
+  | Nil -> true
+  | Cons (_, _) -> false
+
+  (** val mem : key -> 'a1 t -> bool **)
+
+  let rec mem k = function
+  | Nil -> false
+  | Cons (p, l) ->
+    let (k', _) = p in
+    (match X.compare k k' with
+     | LT -> false
+     | EQ -> true
+     | GT -> mem k l)
+
+  type 'elt coq_R_mem =
+  | R_mem_0 of 'elt t
+  | R_mem_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+  | R_mem_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+  | R_mem_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * bool * 'elt coq_R_mem
+
+  (** val coq_R_mem_rect :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2) -> 'a1 t ->
+      bool -> 'a1 coq_R_mem -> 'a2 **)
+
+  let rec coq_R_mem_rect k f f0 f1 f2 _ _ = function
+  | R_mem_0 s -> f s __
+  | R_mem_1 (s, k', _x, l) -> f0 s k' _x l __ __ __
+  | R_mem_2 (s, k', _x, l) -> f1 s k' _x l __ __ __
+  | R_mem_3 (s, k', _x, l, _res, r0) ->
+    f2 s k' _x l __ __ __ _res r0 (coq_R_mem_rect k f f0 f1 f2 l _res r0)
+
+  (** val coq_R_mem_rec :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2) -> 'a1 t ->
+      bool -> 'a1 coq_R_mem -> 'a2 **)
+
+  let rec coq_R_mem_rec k f f0 f1 f2 _ _ = function
+  | R_mem_0 s -> f s __
+  | R_mem_1 (s, k', _x, l) -> f0 s k' _x l __ __ __
+  | R_mem_2 (s, k', _x, l) -> f1 s k' _x l __ __ __
+  | R_mem_3 (s, k', _x, l, _res, r0) ->
+    f2 s k' _x l __ __ __ _res r0 (coq_R_mem_rec k f f0 f1 f2 l _res r0)
+
+  (** val mem_rect :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+  let rec mem_rect k f2 f1 f0 f s =
+    let f3 = f2 s in
+    let f4 = f1 s in
+    let f5 = f0 s in
+    let f6 = f s in
+    (match s with
+     | Nil -> f3 __
+     | Cons (p, l) ->
+       let (t0, e) = p in
+       let f7 = f6 t0 e l __ in
+       let f8 = fun _ _ -> let hrec = mem_rect k f2 f1 f0 f l in f7 __ __ hrec
+       in
+       let f9 = f5 t0 e l __ in
+       let f10 = f4 t0 e l __ in
+       (match X.compare k t0 with
+        | LT -> f10 __ __
+        | EQ -> f9 __ __
+        | GT -> f8 __ __))
+
+  (** val mem_rec :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+  let mem_rec =
+    mem_rect
+
+  (** val coq_R_mem_correct : key -> 'a1 t -> bool -> 'a1 coq_R_mem **)
+
+  let coq_R_mem_correct k s _res =
+    Obj.magic mem_rect k (fun y _ _ _ -> R_mem_0 y)
+      (fun y y0 y1 y2 _ _ _ _ _ -> R_mem_1 (y, y0, y1, y2))
+      (fun y y0 y1 y2 _ _ _ _ _ -> R_mem_2 (y, y0, y1, y2))
+      (fun y y0 y1 y2 _ _ _ y6 _ _ -> R_mem_3 (y, y0, y1, y2, (mem k y2),
+      (y6 (mem k y2) __))) s _res __
+
+  (** val find : key -> 'a1 t -> 'a1 option **)
+
+  let rec find k = function
+  | Nil -> None
+  | Cons (p, s') ->
+    let (k', x) = p in
+    (match X.compare k k' with
+     | LT -> None
+     | EQ -> Some x
+     | GT -> find k s')
+
+  type 'elt coq_R_find =
+  | R_find_0 of 'elt t
+  | R_find_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+  | R_find_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+  | R_find_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * 'elt option
+     * 'elt coq_R_find
+
+  (** val coq_R_find_rect :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find -> 'a2 -> 'a2) -> 'a1
+      t -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
+
+  let rec coq_R_find_rect k f f0 f1 f2 _ _ = function
+  | R_find_0 s -> f s __
+  | R_find_1 (s, k', x, s') -> f0 s k' x s' __ __ __
+  | R_find_2 (s, k', x, s') -> f1 s k' x s' __ __ __
+  | R_find_3 (s, k', x, s', _res, r0) ->
+    f2 s k' x s' __ __ __ _res r0 (coq_R_find_rect k f f0 f1 f2 s' _res r0)
+
+  (** val coq_R_find_rec :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find -> 'a2 -> 'a2) -> 'a1
+      t -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
+
+  let rec coq_R_find_rec k f f0 f1 f2 _ _ = function
+  | R_find_0 s -> f s __
+  | R_find_1 (s, k', x, s') -> f0 s k' x s' __ __ __
+  | R_find_2 (s, k', x, s') -> f1 s k' x s' __ __ __
+  | R_find_3 (s, k', x, s', _res, r0) ->
+    f2 s k' x s' __ __ __ _res r0 (coq_R_find_rec k f f0 f1 f2 s' _res r0)
+
+  (** val find_rect :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+  let rec find_rect k f2 f1 f0 f s =
+    let f3 = f2 s in
+    let f4 = f1 s in
+    let f5 = f0 s in
+    let f6 = f s in
+    (match s with
+     | Nil -> f3 __
+     | Cons (p, l) ->
+       let (t0, e) = p in
+       let f7 = f6 t0 e l __ in
+       let f8 = fun _ _ ->
+         let hrec = find_rect k f2 f1 f0 f l in f7 __ __ hrec
+       in
+       let f9 = f5 t0 e l __ in
+       let f10 = f4 t0 e l __ in
+       (match X.compare k t0 with
+        | LT -> f10 __ __
+        | EQ -> f9 __ __
+        | GT -> f8 __ __))
+
+  (** val find_rec :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+  let find_rec =
+    find_rect
+
+  (** val coq_R_find_correct :
+      key -> 'a1 t -> 'a1 option -> 'a1 coq_R_find **)
+
+  let coq_R_find_correct k s _res =
+    Obj.magic find_rect k (fun y _ _ _ -> R_find_0 y)
+      (fun y y0 y1 y2 _ _ _ _ _ -> R_find_1 (y, y0, y1, y2))
+      (fun y y0 y1 y2 _ _ _ _ _ -> R_find_2 (y, y0, y1, y2))
+      (fun y y0 y1 y2 _ _ _ y6 _ _ -> R_find_3 (y, y0, y1, y2, (find k y2),
+      (y6 (find k y2) __))) s _res __
+
+  (** val add : key -> 'a1 -> 'a1 t -> 'a1 t **)
+
+  let rec add k x s = match s with
+  | Nil -> Cons ((k, x), Nil)
+  | Cons (p, l) ->
+    let (k', y) = p in
+    (match X.compare k k' with
+     | LT -> Cons ((k, x), s)
+     | EQ -> Cons ((k, x), l)
+     | GT -> Cons ((k', y), (add k x l)))
+
+  type 'elt coq_R_add =
+  | R_add_0 of 'elt t
+  | R_add_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+  | R_add_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+  | R_add_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * 'elt t
+     * 'elt coq_R_add
+
+  (** val coq_R_add_rect :
+      key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_add -> 'a2 ->
+      'a2) -> 'a1 t -> 'a1 t -> 'a1 coq_R_add -> 'a2 **)
+
+  let rec coq_R_add_rect k x f f0 f1 f2 _ _ = function
+  | R_add_0 s -> f s __
+  | R_add_1 (s, k', y, l) -> f0 s k' y l __ __ __
+  | R_add_2 (s, k', y, l) -> f1 s k' y l __ __ __
+  | R_add_3 (s, k', y, l, _res, r0) ->
+    f2 s k' y l __ __ __ _res r0 (coq_R_add_rect k x f f0 f1 f2 l _res r0)
+
+  (** val coq_R_add_rec :
+      key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_add -> 'a2 ->
+      'a2) -> 'a1 t -> 'a1 t -> 'a1 coq_R_add -> 'a2 **)
+
+  let rec coq_R_add_rec k x f f0 f1 f2 _ _ = function
+  | R_add_0 s -> f s __
+  | R_add_1 (s, k', y, l) -> f0 s k' y l __ __ __
+  | R_add_2 (s, k', y, l) -> f1 s k' y l __ __ __
+  | R_add_3 (s, k', y, l, _res, r0) ->
+    f2 s k' y l __ __ __ _res r0 (coq_R_add_rec k x f f0 f1 f2 l _res r0)
+
+  (** val add_rect :
+      key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+  let rec add_rect k x f2 f1 f0 f s =
+    let f3 = f2 s in
+    let f4 = f1 s in
+    let f5 = f0 s in
+    let f6 = f s in
+    (match s with
+     | Nil -> f3 __
+     | Cons (p, l) ->
+       let (t0, e) = p in
+       let f7 = f6 t0 e l __ in
+       let f8 = fun _ _ ->
+         let hrec = add_rect k x f2 f1 f0 f l in f7 __ __ hrec
+       in
+       let f9 = f5 t0 e l __ in
+       let f10 = f4 t0 e l __ in
+       (match X.compare k t0 with
+        | LT -> f10 __ __
+        | EQ -> f9 __ __
+        | GT -> f8 __ __))
+
+  (** val add_rec :
+      key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+  let add_rec =
+    add_rect
+
+  (** val coq_R_add_correct :
+      key -> 'a1 -> 'a1 t -> 'a1 t -> 'a1 coq_R_add **)
+
+  let coq_R_add_correct k x s _res =
+    add_rect k x (fun y _ _ _ -> R_add_0 y) (fun y y0 y1 y2 _ _ _ _ _ ->
+      R_add_1 (y, y0, y1, y2)) (fun y y0 y1 y2 _ _ _ _ _ -> R_add_2 (y, y0,
+      y1, y2)) (fun y y0 y1 y2 _ _ _ y6 _ _ -> R_add_3 (y, y0, y1, y2,
+      (add k x y2), (y6 (add k x y2) __))) s _res __
+
+  (** val remove : key -> 'a1 t -> 'a1 t **)
+
+  let rec remove k s = match s with
+  | Nil -> Nil
+  | Cons (p, l) ->
+    let (k', x) = p in
+    (match X.compare k k' with
+     | LT -> s
+     | EQ -> l
+     | GT -> Cons ((k', x), (remove k l)))
+
+  type 'elt coq_R_remove =
+  | R_remove_0 of 'elt t
+  | R_remove_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+  | R_remove_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+  | R_remove_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * 'elt t
+     * 'elt coq_R_remove
+
+  (** val coq_R_remove_rect :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_remove -> 'a2 -> 'a2) -> 'a1 t
+      -> 'a1 t -> 'a1 coq_R_remove -> 'a2 **)
+
+  let rec coq_R_remove_rect k f f0 f1 f2 _ _ = function
+  | R_remove_0 s -> f s __
+  | R_remove_1 (s, k', x, l) -> f0 s k' x l __ __ __
+  | R_remove_2 (s, k', x, l) -> f1 s k' x l __ __ __
+  | R_remove_3 (s, k', x, l, _res, r0) ->
+    f2 s k' x l __ __ __ _res r0 (coq_R_remove_rect k f f0 f1 f2 l _res r0)
+
+  (** val coq_R_remove_rec :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_remove -> 'a2 -> 'a2) -> 'a1 t
+      -> 'a1 t -> 'a1 coq_R_remove -> 'a2 **)
+
+  let rec coq_R_remove_rec k f f0 f1 f2 _ _ = function
+  | R_remove_0 s -> f s __
+  | R_remove_1 (s, k', x, l) -> f0 s k' x l __ __ __
+  | R_remove_2 (s, k', x, l) -> f1 s k' x l __ __ __
+  | R_remove_3 (s, k', x, l, _res, r0) ->
+    f2 s k' x l __ __ __ _res r0 (coq_R_remove_rec k f f0 f1 f2 l _res r0)
+
+  (** val remove_rect :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+  let rec remove_rect k f2 f1 f0 f s =
+    let f3 = f2 s in
+    let f4 = f1 s in
+    let f5 = f0 s in
+    let f6 = f s in
+    (match s with
+     | Nil -> f3 __
+     | Cons (p, l) ->
+       let (t0, e) = p in
+       let f7 = f6 t0 e l __ in
+       let f8 = fun _ _ ->
+         let hrec = remove_rect k f2 f1 f0 f l in f7 __ __ hrec
+       in
+       let f9 = f5 t0 e l __ in
+       let f10 = f4 t0 e l __ in
+       (match X.compare k t0 with
+        | LT -> f10 __ __
+        | EQ -> f9 __ __
+        | GT -> f8 __ __))
+
+  (** val remove_rec :
+      key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+  let remove_rec =
+    remove_rect
+
+  (** val coq_R_remove_correct : key -> 'a1 t -> 'a1 t -> 'a1 coq_R_remove **)
+
+  let coq_R_remove_correct k s _res =
+    Obj.magic remove_rect k (fun y _ _ _ -> R_remove_0 y)
+      (fun y y0 y1 y2 _ _ _ _ _ -> R_remove_1 (y, y0, y1, y2))
+      (fun y y0 y1 y2 _ _ _ _ _ -> R_remove_2 (y, y0, y1, y2))
+      (fun y y0 y1 y2 _ _ _ y6 _ _ -> R_remove_3 (y, y0, y1, y2,
+      (remove k y2), (y6 (remove k y2) __))) s _res __
+
+  (** val elements : 'a1 t -> 'a1 t **)
+
+  let elements m =
+    m
+
+  (** val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2 **)
+
+  let rec fold f m acc =
+    match m with
+    | Nil -> acc
+    | Cons (p, m') -> let (k, e) = p in fold f m' (f k e acc)
+
+  type ('elt, 'a) coq_R_fold =
+  | R_fold_0 of 'elt t * 'a
+  | R_fold_1 of 'elt t * 'a * X.t * 'elt * (X.t * 'elt) list * 'a
+     * ('elt, 'a) coq_R_fold
+
+  (** val coq_R_fold_rect :
+      (key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
+      'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a2 -> ('a1, 'a2)
+      coq_R_fold -> 'a3 -> 'a3) -> 'a1 t -> 'a2 -> 'a2 -> ('a1, 'a2)
+      coq_R_fold -> 'a3 **)
+
+  let rec coq_R_fold_rect f f0 f1 _ _ _ = function
+  | R_fold_0 (m, acc) -> f0 m acc __
+  | R_fold_1 (m, acc, k, e, m', _res, r0) ->
+    f1 m acc k e m' __ _res r0
+      (coq_R_fold_rect f f0 f1 m' (f k e acc) _res r0)
+
+  (** val coq_R_fold_rec :
+      (key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
+      'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a2 -> ('a1, 'a2)
+      coq_R_fold -> 'a3 -> 'a3) -> 'a1 t -> 'a2 -> 'a2 -> ('a1, 'a2)
+      coq_R_fold -> 'a3 **)
+
+  let rec coq_R_fold_rec f f0 f1 _ _ _ = function
+  | R_fold_0 (m, acc) -> f0 m acc __
+  | R_fold_1 (m, acc, k, e, m', _res, r0) ->
+    f1 m acc k e m' __ _res r0 (coq_R_fold_rec f f0 f1 m' (f k e acc) _res r0)
+
+  (** val fold_rect :
+      (key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
+      'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a3 -> 'a3) -> 'a1 t ->
+      'a2 -> 'a3 **)
+
+  let rec fold_rect f1 f0 f m acc =
+    let f2 = f0 m acc in
+    let f3 = f m acc in
+    (match m with
+     | Nil -> f2 __
+     | Cons (p, l) ->
+       let (t0, e) = p in
+       let f4 = f3 t0 e l __ in
+       let hrec = fold_rect f1 f0 f l (f1 t0 e acc) in f4 hrec)
+
+  (** val fold_rec :
+      (key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
+      'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a3 -> 'a3) -> 'a1 t ->
+      'a2 -> 'a3 **)
+
+  let fold_rec =
+    fold_rect
+
+  (** val coq_R_fold_correct :
+      (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2 -> ('a1, 'a2)
+      coq_R_fold **)
+
+  let coq_R_fold_correct f m acc _res =
+    fold_rect f (fun y y0 _ _ _ -> R_fold_0 (y, y0))
+      (fun y y0 y1 y2 y3 _ y5 _ _ -> R_fold_1 (y, y0, y1, y2, y3,
+      (fold f y3 (f y1 y2 y0)), (y5 (fold f y3 (f y1 y2 y0)) __))) m acc _res
+      __
+
+  (** val equal : ('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool **)
+
+  let rec equal cmp m m' =
+    match m with
+    | Nil -> (match m' with
+              | Nil -> true
+              | Cons (_, _) -> false)
+    | Cons (p, l) ->
+      let (x, e) = p in
+      (match m' with
+       | Nil -> false
+       | Cons (p0, l') ->
+         let (x', e') = p0 in
+         (match X.compare x x' with
+          | EQ -> if cmp e e' then equal cmp l l' else false
+          | _ -> false))
+
+  type 'elt coq_R_equal =
+  | R_equal_0 of 'elt t * 'elt t
+  | R_equal_1 of 'elt t * 'elt t * X.t * 'elt * (X.t * 'elt) list * X.t
+     * 'elt * (X.t * 'elt) list * bool * 'elt coq_R_equal
+  | R_equal_2 of 'elt t * 'elt t * X.t * 'elt * (X.t * 'elt) list * X.t
+     * 'elt * (X.t * 'elt) list * X.t compare1
+  | R_equal_3 of 'elt t * 'elt t * 'elt t * 'elt t
+
+  (** val coq_R_equal_rect :
+      ('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
+      -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> bool -> 'a1 coq_R_equal -> 'a2 ->
+      'a2) -> ('a1 t -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t
+      -> 'a1 -> (X.t * 'a1) list -> __ -> X.t compare1 -> __ -> __ -> 'a2) ->
+      ('a1 t -> 'a1 t -> 'a1 t -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t ->
+      'a1 t -> bool -> 'a1 coq_R_equal -> 'a2 **)
+
+  let rec coq_R_equal_rect cmp f f0 f1 f2 _ _ _ = function
+  | R_equal_0 (m, m') -> f m m' __ __
+  | R_equal_1 (m, m', x, e, l, x', e', l', _res, r0) ->
+    f0 m m' x e l __ x' e' l' __ __ __ _res r0
+      (coq_R_equal_rect cmp f f0 f1 f2 l l' _res r0)
+  | R_equal_2 (m, m', x, e, l, x', e', l', _x) ->
+    f1 m m' x e l __ x' e' l' __ _x __ __
+  | R_equal_3 (m, m', _x, _x0) -> f2 m m' _x __ _x0 __ __
+
+  (** val coq_R_equal_rec :
+      ('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
+      -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> bool -> 'a1 coq_R_equal -> 'a2 ->
+      'a2) -> ('a1 t -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t
+      -> 'a1 -> (X.t * 'a1) list -> __ -> X.t compare1 -> __ -> __ -> 'a2) ->
+      ('a1 t -> 'a1 t -> 'a1 t -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t ->
+      'a1 t -> bool -> 'a1 coq_R_equal -> 'a2 **)
+
+  let rec coq_R_equal_rec cmp f f0 f1 f2 _ _ _ = function
+  | R_equal_0 (m, m') -> f m m' __ __
+  | R_equal_1 (m, m', x, e, l, x', e', l', _res, r0) ->
+    f0 m m' x e l __ x' e' l' __ __ __ _res r0
+      (coq_R_equal_rec cmp f f0 f1 f2 l l' _res r0)
+  | R_equal_2 (m, m', x, e, l, x', e', l', _x) ->
+    f1 m m' x e l __ x' e' l' __ _x __ __
+  | R_equal_3 (m, m', _x, _x0) -> f2 m m' _x __ _x0 __ __
+
+  (** val equal_rect :
+      ('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
+      -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> ('a1 t -> 'a1 t ->
+      X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> X.t compare1 -> __ -> __ -> 'a2) -> ('a1 t -> 'a1 t -> 'a1 t
+      -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t -> 'a1 t -> 'a2 **)
+
+  let rec equal_rect cmp f2 f1 f0 f m m' =
+    let f3 = f2 m m' in
+    let f4 = f1 m m' in
+    let f5 = f0 m m' in
+    let f6 = f m m' in
+    let f7 = f6 m __ in
+    let f8 = f7 m' __ in
+    (match m with
+     | Nil ->
+       let f9 = f3 __ in (match m' with
+                          | Nil -> f9 __
+                          | Cons (_, _) -> f8 __)
+     | Cons (p, l) ->
+       let (t0, e) = p in
+       let f9 = f5 t0 e l __ in
+       let f10 = f4 t0 e l __ in
+       (match m' with
+        | Nil -> f8 __
+        | Cons (p0, l0) ->
+          let (t1, e0) = p0 in
+          let f11 = f9 t1 e0 l0 __ in
+          let f12 = let _x = X.compare t0 t1 in f11 _x __ in
+          let f13 = f10 t1 e0 l0 __ in
+          let f14 = fun _ _ ->
+            let hrec = equal_rect cmp f2 f1 f0 f l l0 in f13 __ __ hrec
+          in
+          (match X.compare t0 t1 with
+           | EQ -> f14 __ __
+           | _ -> f12 __)))
+
+  (** val equal_rec :
+      ('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
+      -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
+      (X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> ('a1 t -> 'a1 t ->
+      X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 -> (X.t * 'a1) list
+      -> __ -> X.t compare1 -> __ -> __ -> 'a2) -> ('a1 t -> 'a1 t -> 'a1 t
+      -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t -> 'a1 t -> 'a2 **)
+
+  let equal_rec =
+    equal_rect
+
+  (** val coq_R_equal_correct :
+      ('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool -> 'a1 coq_R_equal **)
+
+  let coq_R_equal_correct cmp m m' _res =
+    equal_rect cmp (fun y y0 _ _ _ _ -> R_equal_0 (y, y0))
+      (fun y y0 y1 y2 y3 _ y5 y6 y7 _ _ _ y11 _ _ -> R_equal_1 (y, y0, y1,
+      y2, y3, y5, y6, y7, (equal cmp y3 y7), (y11 (equal cmp y3 y7) __)))
+      (fun y y0 y1 y2 y3 _ y5 y6 y7 _ y9 _ _ _ _ -> R_equal_2 (y, y0, y1, y2,
+      y3, y5, y6, y7, y9)) (fun y y0 y1 _ y3 _ _ _ _ -> R_equal_3 (y, y0, y1,
+      y3)) m m' _res __
+
+  (** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+
+  let rec map f = function
+  | Nil -> Nil
+  | Cons (p, m') -> let (k, e) = p in Cons ((k, (f e)), (map f m'))
+
+  (** val mapi : (key -> 'a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+
+  let rec mapi f = function
+  | Nil -> Nil
+  | Cons (p, m') -> let (k, e) = p in Cons ((k, (f k e)), (mapi f m'))
+
+  (** val option_cons :
+      key -> 'a1 option -> (key * 'a1) list -> (key * 'a1) list **)
+
+  let option_cons k o l =
+    match o with
+    | Some e -> Cons ((k, e), l)
+    | None -> l
+
+  (** val map2_l :
+      ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a3 t **)
+
+  let rec map2_l f = function
+  | Nil -> Nil
+  | Cons (p, l) ->
+    let (k, e) = p in option_cons k (f (Some e) None) (map2_l f l)
+
+  (** val map2_r :
+      ('a1 option -> 'a2 option -> 'a3 option) -> 'a2 t -> 'a3 t **)
+
+  let rec map2_r f = function
+  | Nil -> Nil
+  | Cons (p, l') ->
+    let (k, e') = p in option_cons k (f None (Some e')) (map2_r f l')
+
+  (** val map2 :
+      ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t -> 'a3 t **)
+
+  let rec map2 f m = match m with
+  | Nil -> map2_r f
+  | Cons (p, l) ->
+    let (k, e) = p in
+    let rec map2_aux m' = match m' with
+    | Nil -> map2_l f m
+    | Cons (p0, l') ->
+      let (k', e') = p0 in
+      (match X.compare k k' with
+       | LT -> option_cons k (f (Some e) None) (map2 f l m')
+       | EQ -> option_cons k (f (Some e) (Some e')) (map2 f l l')
+       | GT -> option_cons k' (f None (Some e')) (map2_aux l'))
+    in map2_aux
+
+  (** val combine : 'a1 t -> 'a2 t -> ('a1 option * 'a2 option) t **)
+
+  let rec combine m = match m with
+  | Nil -> map (fun e' -> (None, (Some e')))
+  | Cons (p, l) ->
+    let (k, e) = p in
+    let rec combine_aux m' = match m' with
+    | Nil -> map (fun e0 -> ((Some e0), None)) m
+    | Cons (p0, l') ->
+      let (k', e') = p0 in
+      (match X.compare k k' with
+       | LT -> Cons ((k, ((Some e), None)), (combine l m'))
+       | EQ -> Cons ((k, ((Some e), (Some e'))), (combine l l'))
+       | GT -> Cons ((k', (None, (Some e'))), (combine_aux l')))
+    in combine_aux
+
+  (** val fold_right_pair :
+      ('a1 -> 'a2 -> 'a3 -> 'a3) -> ('a1 * 'a2) list -> 'a3 -> 'a3 **)
+
+  let fold_right_pair f l i =
+    fold_right (fun p -> f (fst p) (snd p)) i l
+
+  (** val map2_alt :
+      ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t ->
+      (key * 'a3) list **)
+
+  let map2_alt f m m' =
+    let m0 = combine m m' in
+    let m1 = map (fun p -> f (fst p) (snd p)) m0 in
+    fold_right_pair option_cons m1 Nil
+
+  (** val at_least_one :
+      'a1 option -> 'a2 option -> ('a1 option * 'a2 option) option **)
+
+  let at_least_one o o' =
+    match o with
+    | Some _ -> Some (o, o')
+    | None -> (match o' with
+               | Some _ -> Some (o, o')
+               | None -> None)
+
+  (** val at_least_one_then_f :
+      ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 option -> 'a2 option ->
+      'a3 option **)
+
+  let at_least_one_then_f f o o' =
+    match o with
+    | Some _ -> f o o'
+    | None -> (match o' with
+               | Some _ -> f o o'
+               | None -> None)
  end
 
-module Var = 
- struct 
-  (** val _true : int **)
-  
-  let _true =
-    (ExtrNative.of_uint(0))
-  
-  (** val _false : int **)
-  
-  let _false =
-    (ExtrNative.of_uint(1))
-  
-  (** val interp : Valuation.t -> int -> bool **)
-  
-  let interp rho x =
-    rho x
+module type Int =
+ sig
+  type t
+
+  val i2z : t -> z
+
+  val _0 : t
+
+  val _1 : t
+
+  val _2 : t
+
+  val _3 : t
+
+  val add : t -> t -> t
+
+  val opp : t -> t
+
+  val sub : t -> t -> t
+
+  val mul : t -> t -> t
+
+  val max : t -> t -> t
+
+  val eqb : t -> t -> bool
+
+  val ltb : t -> t -> bool
+
+  val leb : t -> t -> bool
+
+  val gt_le_dec : t -> t -> sumbool
+
+  val ge_lt_dec : t -> t -> sumbool
+
+  val eq_dec : t -> t -> sumbool
  end
 
-module Lit = 
- struct 
-  (** val is_pos : int -> bool **)
-  
-  let is_pos l =
-    is_even l
-  
-  (** val blit : int -> int **)
-  
-  let blit l =
-    lsr0 l (ExtrNative.of_uint(1))
-  
-  (** val lit : int -> int **)
-  
-  let lit x =
-    lsl0 x (ExtrNative.of_uint(1))
-  
-  (** val neg : int -> int **)
-  
-  let neg l =
-    lxor0 l (ExtrNative.of_uint(1))
-  
-  (** val nlit : int -> int **)
-  
-  let nlit x =
-    neg (lit x)
-  
-  (** val _true : int **)
-  
+module Z_as_Int =
+ struct
+  type t = z
+
+  (** val _0 : z **)
+
+  let _0 =
+    Z0
+
+  (** val _1 : z **)
+
+  let _1 =
+    Zpos XH
+
+  (** val _2 : z **)
+
+  let _2 =
+    Zpos (XO XH)
+
+  (** val _3 : z **)
+
+  let _3 =
+    Zpos (XI XH)
+
+  (** val add : z -> z -> z **)
+
+  let add =
+    Z.add
+
+  (** val opp : z -> z **)
+
+  let opp =
+    Z.opp
+
+  (** val sub : z -> z -> z **)
+
+  let sub =
+    Z.sub
+
+  (** val mul : z -> z -> z **)
+
+  let mul =
+    Z.mul
+
+  (** val max : z -> z -> z **)
+
+  let max =
+    Z.max
+
+  (** val eqb : z -> z -> bool **)
+
+  let eqb =
+    Z.eqb
+
+  (** val ltb : z -> z -> bool **)
+
+  let ltb =
+    Z.ltb
+
+  (** val leb : z -> z -> bool **)
+
+  let leb =
+    Z.leb
+
+  (** val eq_dec : z -> z -> sumbool **)
+
+  let eq_dec =
+    Z.eq_dec
+
+  (** val gt_le_dec : z -> z -> sumbool **)
+
+  let gt_le_dec i j =
+    let b = Z.ltb j i in if b then Left else Right
+
+  (** val ge_lt_dec : z -> z -> sumbool **)
+
+  let ge_lt_dec i j =
+    let b = Z.ltb i j in if b then Right else Left
+
+  (** val i2z : t -> z **)
+
+  let i2z n =
+    n
+ end
+
+module Coq_Raw =
+ functor (I:Int) ->
+ functor (X:OrderedType) ->
+ struct
+  type key = X.t
+
+  type 'elt tree =
+  | Leaf
+  | Node of 'elt tree * key * 'elt * 'elt tree * I.t
+
+  (** val tree_rect :
+      'a2 -> ('a1 tree -> 'a2 -> key -> 'a1 -> 'a1 tree -> 'a2 -> I.t -> 'a2)
+      -> 'a1 tree -> 'a2 **)
+
+  let rec tree_rect f f0 = function
+  | Leaf -> f
+  | Node (t1, k, y, t2, t3) ->
+    f0 t1 (tree_rect f f0 t1) k y t2 (tree_rect f f0 t2) t3
+
+  (** val tree_rec :
+      'a2 -> ('a1 tree -> 'a2 -> key -> 'a1 -> 'a1 tree -> 'a2 -> I.t -> 'a2)
+      -> 'a1 tree -> 'a2 **)
+
+  let rec tree_rec f f0 = function
+  | Leaf -> f
+  | Node (t1, k, y, t2, t3) ->
+    f0 t1 (tree_rec f f0 t1) k y t2 (tree_rec f f0 t2) t3
+
+  (** val height : 'a1 tree -> I.t **)
+
+  let height = function
+  | Leaf -> I._0
+  | Node (_, _, _, _, h) -> h
+
+  (** val cardinal : 'a1 tree -> nat **)
+
+  let rec cardinal = function
+  | Leaf -> O
+  | Node (l, _, _, r, _) -> S (add (cardinal l) (cardinal r))
+
+  (** val empty : 'a1 tree **)
+
+  let empty =
+    Leaf
+
+  (** val is_empty : 'a1 tree -> bool **)
+
+  let is_empty = function
+  | Leaf -> true
+  | Node (_, _, _, _, _) -> false
+
+  (** val mem : X.t -> 'a1 tree -> bool **)
+
+  let rec mem x = function
+  | Leaf -> false
+  | Node (l, y, _, r, _) ->
+    (match X.compare x y with
+     | LT -> mem x l
+     | EQ -> true
+     | GT -> mem x r)
+
+  (** val find : X.t -> 'a1 tree -> 'a1 option **)
+
+  let rec find x = function
+  | Leaf -> None
+  | Node (l, y, d, r, _) ->
+    (match X.compare x y with
+     | LT -> find x l
+     | EQ -> Some d
+     | GT -> find x r)
+
+  (** val create : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+  let create l x e r =
+    Node (l, x, e, r, (I.add (I.max (height l) (height r)) I._1))
+
+  (** val assert_false : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+  let assert_false =
+    create
+
+  (** val bal : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+  let bal l x d r =
+    let hl = height l in
+    let hr = height r in
+    (match I.gt_le_dec hl (I.add hr I._2) with
+     | Left ->
+       (match l with
+        | Leaf -> assert_false l x d r
+        | Node (ll, lx, ld, lr, _) ->
+          (match I.ge_lt_dec (height ll) (height lr) with
+           | Left -> create ll lx ld (create lr x d r)
+           | Right ->
+             (match lr with
+              | Leaf -> assert_false l x d r
+              | Node (lrl, lrx, lrd, lrr, _) ->
+                create (create ll lx ld lrl) lrx lrd (create lrr x d r))))
+     | Right ->
+       (match I.gt_le_dec hr (I.add hl I._2) with
+        | Left ->
+          (match r with
+           | Leaf -> assert_false l x d r
+           | Node (rl, rx, rd, rr, _) ->
+             (match I.ge_lt_dec (height rr) (height rl) with
+              | Left -> create (create l x d rl) rx rd rr
+              | Right ->
+                (match rl with
+                 | Leaf -> assert_false l x d r
+                 | Node (rll, rlx, rld, rlr, _) ->
+                   create (create l x d rll) rlx rld (create rlr rx rd rr))))
+        | Right -> create l x d r))
+
+  (** val add : key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+  let rec add x d = function
+  | Leaf -> Node (Leaf, x, d, Leaf, I._1)
+  | Node (l, y, d', r, h) ->
+    (match X.compare x y with
+     | LT -> bal (add x d l) y d' r
+     | EQ -> Node (l, y, d, r, h)
+     | GT -> bal l y d' (add x d r))
+
+  (** val remove_min :
+      'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree * (key * 'a1) **)
+
+  let rec remove_min l x d r =
+    match l with
+    | Leaf -> (r, (x, d))
+    | Node (ll, lx, ld, lr, _) ->
+      let (l', m) = remove_min ll lx ld lr in ((bal l' x d r), m)
+
+  (** val merge : 'a1 tree -> 'a1 tree -> 'a1 tree **)
+
+  let merge s1 s2 =
+    match s1 with
+    | Leaf -> s2
+    | Node (_, _, _, _, _) ->
+      (match s2 with
+       | Leaf -> s1
+       | Node (l2, x2, d2, r2, _) ->
+         let (s2', p) = remove_min l2 x2 d2 r2 in
+         let (x, d) = p in bal s1 x d s2')
+
+  (** val remove : X.t -> 'a1 tree -> 'a1 tree **)
+
+  let rec remove x = function
+  | Leaf -> Leaf
+  | Node (l, y, d, r, _) ->
+    (match X.compare x y with
+     | LT -> bal (remove x l) y d r
+     | EQ -> merge l r
+     | GT -> bal l y d (remove x r))
+
+  (** val join : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+  let rec join l = match l with
+  | Leaf -> add
+  | Node (ll, lx, ld, lr, lh) ->
+    (fun x d ->
+      let rec join_aux r = match r with
+      | Leaf -> add x d l
+      | Node (rl, rx, rd, rr, rh) ->
+        (match I.gt_le_dec lh (I.add rh I._2) with
+         | Left -> bal ll lx ld (join lr x d r)
+         | Right ->
+           (match I.gt_le_dec rh (I.add lh I._2) with
+            | Left -> bal (join_aux rl) rx rd rr
+            | Right -> create l x d r))
+      in join_aux)
+
+  type 'elt triple = { t_left : 'elt tree; t_opt : 'elt option;
+                       t_right : 'elt tree }
+
+  (** val t_left : 'a1 triple -> 'a1 tree **)
+
+  let t_left t0 =
+    t0.t_left
+
+  (** val t_opt : 'a1 triple -> 'a1 option **)
+
+  let t_opt t0 =
+    t0.t_opt
+
+  (** val t_right : 'a1 triple -> 'a1 tree **)
+
+  let t_right t0 =
+    t0.t_right
+
+  (** val split : X.t -> 'a1 tree -> 'a1 triple **)
+
+  let rec split x = function
+  | Leaf -> { t_left = Leaf; t_opt = None; t_right = Leaf }
+  | Node (l, y, d, r, _) ->
+    (match X.compare x y with
+     | LT ->
+       let { t_left = ll; t_opt = o; t_right = rl } = split x l in
+       { t_left = ll; t_opt = o; t_right = (join rl y d r) }
+     | EQ -> { t_left = l; t_opt = (Some d); t_right = r }
+     | GT ->
+       let { t_left = rl; t_opt = o; t_right = rr } = split x r in
+       { t_left = (join l y d rl); t_opt = o; t_right = rr })
+
+  (** val concat : 'a1 tree -> 'a1 tree -> 'a1 tree **)
+
+  let concat m1 m2 =
+    match m1 with
+    | Leaf -> m2
+    | Node (_, _, _, _, _) ->
+      (match m2 with
+       | Leaf -> m1
+       | Node (l2, x2, d2, r2, _) ->
+         let (m2', xd) = remove_min l2 x2 d2 r2 in
+         join m1 (fst xd) (snd xd) m2')
+
+  (** val elements_aux : (key * 'a1) list -> 'a1 tree -> (key * 'a1) list **)
+
+  let rec elements_aux acc = function
+  | Leaf -> acc
+  | Node (l, x, d, r, _) ->
+    elements_aux (Cons ((x, d), (elements_aux acc r))) l
+
+  (** val elements : 'a1 tree -> (key * 'a1) list **)
+
+  let elements m =
+    elements_aux Nil m
+
+  (** val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 tree -> 'a2 -> 'a2 **)
+
+  let rec fold f m a =
+    match m with
+    | Leaf -> a
+    | Node (l, x, d, r, _) -> fold f r (f x d (fold f l a))
+
+  type 'elt enumeration =
+  | End
+  | More of key * 'elt * 'elt tree * 'elt enumeration
+
+  (** val enumeration_rect :
+      'a2 -> (key -> 'a1 -> 'a1 tree -> 'a1 enumeration -> 'a2 -> 'a2) -> 'a1
+      enumeration -> 'a2 **)
+
+  let rec enumeration_rect f f0 = function
+  | End -> f
+  | More (k, e0, t0, e1) -> f0 k e0 t0 e1 (enumeration_rect f f0 e1)
+
+  (** val enumeration_rec :
+      'a2 -> (key -> 'a1 -> 'a1 tree -> 'a1 enumeration -> 'a2 -> 'a2) -> 'a1
+      enumeration -> 'a2 **)
+
+  let rec enumeration_rec f f0 = function
+  | End -> f
+  | More (k, e0, t0, e1) -> f0 k e0 t0 e1 (enumeration_rec f f0 e1)
+
+  (** val cons : 'a1 tree -> 'a1 enumeration -> 'a1 enumeration **)
+
+  let rec cons m e =
+    match m with
+    | Leaf -> e
+    | Node (l, x, d, r, _) -> cons l (More (x, d, r, e))
+
+  (** val equal_more :
+      ('a1 -> 'a1 -> bool) -> X.t -> 'a1 -> ('a1 enumeration -> bool) -> 'a1
+      enumeration -> bool **)
+
+  let equal_more cmp x1 d1 cont = function
+  | End -> false
+  | More (x2, d2, r2, e3) ->
+    (match X.compare x1 x2 with
+     | EQ -> if cmp d1 d2 then cont (cons r2 e3) else false
+     | _ -> false)
+
+  (** val equal_cont :
+      ('a1 -> 'a1 -> bool) -> 'a1 tree -> ('a1 enumeration -> bool) -> 'a1
+      enumeration -> bool **)
+
+  let rec equal_cont cmp m1 cont e2 =
+    match m1 with
+    | Leaf -> cont e2
+    | Node (l1, x1, d1, r1, _) ->
+      equal_cont cmp l1 (equal_more cmp x1 d1 (equal_cont cmp r1 cont)) e2
+
+  (** val equal_end : 'a1 enumeration -> bool **)
+
+  let equal_end = function
+  | End -> true
+  | More (_, _, _, _) -> false
+
+  (** val equal : ('a1 -> 'a1 -> bool) -> 'a1 tree -> 'a1 tree -> bool **)
+
+  let equal cmp m1 m2 =
+    equal_cont cmp m1 equal_end (cons m2 End)
+
+  (** val map : ('a1 -> 'a2) -> 'a1 tree -> 'a2 tree **)
+
+  let rec map f = function
+  | Leaf -> Leaf
+  | Node (l, x, d, r, h) -> Node ((map f l), x, (f d), (map f r), h)
+
+  (** val mapi : (key -> 'a1 -> 'a2) -> 'a1 tree -> 'a2 tree **)
+
+  let rec mapi f = function
+  | Leaf -> Leaf
+  | Node (l, x, d, r, h) -> Node ((mapi f l), x, (f x d), (mapi f r), h)
+
+  (** val map_option : (key -> 'a1 -> 'a2 option) -> 'a1 tree -> 'a2 tree **)
+
+  let rec map_option f = function
+  | Leaf -> Leaf
+  | Node (l, x, d, r, _) ->
+    (match f x d with
+     | Some d' -> join (map_option f l) x d' (map_option f r)
+     | None -> concat (map_option f l) (map_option f r))
+
+  (** val map2_opt :
+      (key -> 'a1 -> 'a2 option -> 'a3 option) -> ('a1 tree -> 'a3 tree) ->
+      ('a2 tree -> 'a3 tree) -> 'a1 tree -> 'a2 tree -> 'a3 tree **)
+
+  let rec map2_opt f mapl mapr m1 m2 =
+    match m1 with
+    | Leaf -> mapr m2
+    | Node (l1, x1, d1, r1, _) ->
+      (match m2 with
+       | Leaf -> mapl m1
+       | Node (_, _, _, _, _) ->
+         let { t_left = l2'; t_opt = o2; t_right = r2' } = split x1 m2 in
+         (match f x1 d1 o2 with
+          | Some e ->
+            join (map2_opt f mapl mapr l1 l2') x1 e
+              (map2_opt f mapl mapr r1 r2')
+          | None ->
+            concat (map2_opt f mapl mapr l1 l2') (map2_opt f mapl mapr r1 r2')))
+
+  (** val map2 :
+      ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 tree -> 'a2 tree -> 'a3
+      tree **)
+
+  let map2 f =
+    map2_opt (fun _ d o -> f (Some d) o)
+      (map_option (fun _ d -> f (Some d) None))
+      (map_option (fun _ d' -> f None (Some d')))
+
+  module Proofs =
+   struct
+    module MX = OrderedTypeFacts(X)
+
+    module PX = KeyOrderedType(X)
+
+    module L = Raw(X)
+
+    type 'elt coq_R_mem =
+    | R_mem_0 of 'elt tree
+    | R_mem_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t * 
+       bool * 'elt coq_R_mem
+    | R_mem_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+    | R_mem_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t * 
+       bool * 'elt coq_R_mem
+
+    (** val coq_R_mem_rect :
+        X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2
+        -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t ->
+        __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1
+        tree -> I.t -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2)
+        -> 'a1 tree -> bool -> 'a1 coq_R_mem -> 'a2 **)
+
+    let rec coq_R_mem_rect x f f0 f1 f2 _ _ = function
+    | R_mem_0 m -> f m __
+    | R_mem_1 (m, l, y, _x, r0, _x0, _res, r1) ->
+      f0 m l y _x r0 _x0 __ __ __ _res r1
+        (coq_R_mem_rect x f f0 f1 f2 l _res r1)
+    | R_mem_2 (m, l, y, _x, r0, _x0) -> f1 m l y _x r0 _x0 __ __ __
+    | R_mem_3 (m, l, y, _x, r0, _x0, _res, r1) ->
+      f2 m l y _x r0 _x0 __ __ __ _res r1
+        (coq_R_mem_rect x f f0 f1 f2 r0 _res r1)
+
+    (** val coq_R_mem_rec :
+        X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2
+        -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t ->
+        __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1
+        tree -> I.t -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2)
+        -> 'a1 tree -> bool -> 'a1 coq_R_mem -> 'a2 **)
+
+    let rec coq_R_mem_rec x f f0 f1 f2 _ _ = function
+    | R_mem_0 m -> f m __
+    | R_mem_1 (m, l, y, _x, r0, _x0, _res, r1) ->
+      f0 m l y _x r0 _x0 __ __ __ _res r1
+        (coq_R_mem_rec x f f0 f1 f2 l _res r1)
+    | R_mem_2 (m, l, y, _x, r0, _x0) -> f1 m l y _x r0 _x0 __ __ __
+    | R_mem_3 (m, l, y, _x, r0, _x0, _res, r1) ->
+      f2 m l y _x r0 _x0 __ __ __ _res r1
+        (coq_R_mem_rec x f f0 f1 f2 r0 _res r1)
+
+    type 'elt coq_R_find =
+    | R_find_0 of 'elt tree
+    | R_find_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+       * 'elt option * 'elt coq_R_find
+    | R_find_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+    | R_find_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+       * 'elt option * 'elt coq_R_find
+
+    (** val coq_R_find_rect :
+        X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find
+        -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+        I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find
+        -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
+
+    let rec coq_R_find_rect x f f0 f1 f2 _ _ = function
+    | R_find_0 m -> f m __
+    | R_find_1 (m, l, y, d, r0, _x, _res, r1) ->
+      f0 m l y d r0 _x __ __ __ _res r1
+        (coq_R_find_rect x f f0 f1 f2 l _res r1)
+    | R_find_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+    | R_find_3 (m, l, y, d, r0, _x, _res, r1) ->
+      f2 m l y d r0 _x __ __ __ _res r1
+        (coq_R_find_rect x f f0 f1 f2 r0 _res r1)
+
+    (** val coq_R_find_rec :
+        X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find
+        -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+        I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find
+        -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
+
+    let rec coq_R_find_rec x f f0 f1 f2 _ _ = function
+    | R_find_0 m -> f m __
+    | R_find_1 (m, l, y, d, r0, _x, _res, r1) ->
+      f0 m l y d r0 _x __ __ __ _res r1
+        (coq_R_find_rec x f f0 f1 f2 l _res r1)
+    | R_find_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+    | R_find_3 (m, l, y, d, r0, _x, _res, r1) ->
+      f2 m l y d r0 _x __ __ __ _res r1
+        (coq_R_find_rec x f f0 f1 f2 r0 _res r1)
+
+    type 'elt coq_R_bal =
+    | R_bal_0 of 'elt tree * key * 'elt * 'elt tree
+    | R_bal_1 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 
+       'elt * 'elt tree * I.t
+    | R_bal_2 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 
+       'elt * 'elt tree * I.t
+    | R_bal_3 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 
+       'elt * 'elt tree * I.t * 'elt tree * key * 'elt * 'elt tree * 
+       I.t
+    | R_bal_4 of 'elt tree * key * 'elt * 'elt tree
+    | R_bal_5 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 
+       'elt * 'elt tree * I.t
+    | R_bal_6 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 
+       'elt * 'elt tree * I.t
+    | R_bal_7 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 
+       'elt * 'elt tree * I.t * 'elt tree * key * 'elt * 'elt tree * 
+       I.t
+    | R_bal_8 of 'elt tree * key * 'elt * 'elt tree
+
+    (** val coq_R_bal_rect :
+        ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> 'a2) -> ('a1
+        tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> key ->
+        'a1 -> 'a1 tree -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+        I.t -> __ -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1
+        tree -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ ->
+        'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __
+        -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ ->
+        __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ ->
+        __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __
+        -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __
+        -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ ->
+        __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ ->
+        __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2) -> ('a1
+        tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __ -> 'a2) -> 'a1
+        tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_bal -> 'a2 **)
+
+    let coq_R_bal_rect f f0 f1 f2 f3 f4 f5 f6 f7 _ _ _ _ _ = function
+    | R_bal_0 (x, x0, x1, x2) -> f x x0 x1 x2 __ __ __
+    | R_bal_1 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+      f0 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __
+    | R_bal_2 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+      f1 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __ __
+    | R_bal_3 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+      f2 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __ x8 x9 x10 x11 x12 __
+    | R_bal_4 (x, x0, x1, x2) -> f3 x x0 x1 x2 __ __ __ __ __
+    | R_bal_5 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+      f4 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __
+    | R_bal_6 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+      f5 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __ __
+    | R_bal_7 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+      f6 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __ x8 x9 x10 x11 x12 __
+    | R_bal_8 (x, x0, x1, x2) -> f7 x x0 x1 x2 __ __ __ __
+
+    (** val coq_R_bal_rec :
+        ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> 'a2) -> ('a1
+        tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> key ->
+        'a1 -> 'a1 tree -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+        I.t -> __ -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1
+        tree -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ ->
+        'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __
+        -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ ->
+        __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ ->
+        __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __
+        -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __
+        -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ ->
+        __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ ->
+        __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2) -> ('a1
+        tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __ -> 'a2) -> 'a1
+        tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_bal -> 'a2 **)
+
+    let coq_R_bal_rec f f0 f1 f2 f3 f4 f5 f6 f7 _ _ _ _ _ = function
+    | R_bal_0 (x, x0, x1, x2) -> f x x0 x1 x2 __ __ __
+    | R_bal_1 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+      f0 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __
+    | R_bal_2 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+      f1 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __ __
+    | R_bal_3 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+      f2 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __ x8 x9 x10 x11 x12 __
+    | R_bal_4 (x, x0, x1, x2) -> f3 x x0 x1 x2 __ __ __ __ __
+    | R_bal_5 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+      f4 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __
+    | R_bal_6 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+      f5 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __ __
+    | R_bal_7 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+      f6 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __ x8 x9 x10 x11 x12 __
+    | R_bal_8 (x, x0, x1, x2) -> f7 x x0 x1 x2 __ __ __ __
+
+    type 'elt coq_R_add =
+    | R_add_0 of 'elt tree
+    | R_add_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+       * 'elt tree * 'elt coq_R_add
+    | R_add_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+    | R_add_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+       * 'elt tree * 'elt coq_R_add
+
+    (** val coq_R_add_rect :
+        key -> 'a1 -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key
+        -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1
+        coq_R_add -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 ->
+        'a1 tree -> I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree ->
+        key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1
+        coq_R_add -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_add ->
+        'a2 **)
+
+    let rec coq_R_add_rect x d f f0 f1 f2 _ _ = function
+    | R_add_0 m -> f m __
+    | R_add_1 (m, l, y, d', r0, h, _res, r1) ->
+      f0 m l y d' r0 h __ __ __ _res r1
+        (coq_R_add_rect x d f f0 f1 f2 l _res r1)
+    | R_add_2 (m, l, y, d', r0, h) -> f1 m l y d' r0 h __ __ __
+    | R_add_3 (m, l, y, d', r0, h, _res, r1) ->
+      f2 m l y d' r0 h __ __ __ _res r1
+        (coq_R_add_rect x d f f0 f1 f2 r0 _res r1)
+
+    (** val coq_R_add_rec :
+        key -> 'a1 -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key
+        -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1
+        coq_R_add -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 ->
+        'a1 tree -> I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree ->
+        key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1
+        coq_R_add -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_add ->
+        'a2 **)
+
+    let rec coq_R_add_rec x d f f0 f1 f2 _ _ = function
+    | R_add_0 m -> f m __
+    | R_add_1 (m, l, y, d', r0, h, _res, r1) ->
+      f0 m l y d' r0 h __ __ __ _res r1
+        (coq_R_add_rec x d f f0 f1 f2 l _res r1)
+    | R_add_2 (m, l, y, d', r0, h) -> f1 m l y d' r0 h __ __ __
+    | R_add_3 (m, l, y, d', r0, h, _res, r1) ->
+      f2 m l y d' r0 h __ __ __ _res r1
+        (coq_R_add_rec x d f f0 f1 f2 r0 _res r1)
+
+    type 'elt coq_R_remove_min =
+    | R_remove_min_0 of 'elt tree * key * 'elt * 'elt tree
+    | R_remove_min_1 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * 
+       key * 'elt * 'elt tree * I.t * ('elt tree * (key * 'elt))
+       * 'elt coq_R_remove_min * 'elt tree * (key * 'elt)
+
+    (** val coq_R_remove_min_rect :
+        ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> key
+        -> 'a1 -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> ('a1 tree * (key * 'a1)) -> 'a1 coq_R_remove_min -> 'a2 -> 'a1
+        tree -> (key * 'a1) -> __ -> 'a2) -> 'a1 tree -> key -> 'a1 -> 'a1
+        tree -> ('a1 tree * (key * 'a1)) -> 'a1 coq_R_remove_min -> 'a2 **)
+
+    let rec coq_R_remove_min_rect f f0 _ _ _ _ _ = function
+    | R_remove_min_0 (l, x, d, r0) -> f l x d r0 __
+    | R_remove_min_1 (l, x, d, r0, ll, lx, ld, lr, _x, _res, r1, l', m) ->
+      f0 l x d r0 ll lx ld lr _x __ _res r1
+        (coq_R_remove_min_rect f f0 ll lx ld lr _res r1) l' m __
+
+    (** val coq_R_remove_min_rec :
+        ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> key
+        -> 'a1 -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> ('a1 tree * (key * 'a1)) -> 'a1 coq_R_remove_min -> 'a2 -> 'a1
+        tree -> (key * 'a1) -> __ -> 'a2) -> 'a1 tree -> key -> 'a1 -> 'a1
+        tree -> ('a1 tree * (key * 'a1)) -> 'a1 coq_R_remove_min -> 'a2 **)
+
+    let rec coq_R_remove_min_rec f f0 _ _ _ _ _ = function
+    | R_remove_min_0 (l, x, d, r0) -> f l x d r0 __
+    | R_remove_min_1 (l, x, d, r0, ll, lx, ld, lr, _x, _res, r1, l', m) ->
+      f0 l x d r0 ll lx ld lr _x __ _res r1
+        (coq_R_remove_min_rec f f0 ll lx ld lr _res r1) l' m __
+
+    type 'elt coq_R_merge =
+    | R_merge_0 of 'elt tree * 'elt tree
+    | R_merge_1 of 'elt tree * 'elt tree * 'elt tree * key * 'elt * 'elt tree
+       * I.t
+    | R_merge_2 of 'elt tree * 'elt tree * 'elt tree * key * 'elt * 'elt tree
+       * I.t * 'elt tree * key * 'elt * 'elt tree * I.t * 'elt tree
+       * (key * 'elt) * key * 'elt
+
+    (** val coq_R_merge_rect :
+        ('a1 tree -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> 'a1
+        tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2) -> ('a1
+        tree -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a1 tree ->
+        (key * 'a1) -> __ -> key -> 'a1 -> __ -> 'a2) -> 'a1 tree -> 'a1 tree
+        -> 'a1 tree -> 'a1 coq_R_merge -> 'a2 **)
+
+    let coq_R_merge_rect f f0 f1 _ _ _ = function
+    | R_merge_0 (x, x0) -> f x x0 __
+    | R_merge_1 (x, x0, x1, x2, x3, x4, x5) -> f0 x x0 x1 x2 x3 x4 x5 __ __
+    | R_merge_2 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12,
+                 x13, x14) ->
+      f1 x x0 x1 x2 x3 x4 x5 __ x6 x7 x8 x9 x10 __ x11 x12 __ x13 x14 __
+
+    (** val coq_R_merge_rec :
+        ('a1 tree -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> 'a1
+        tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2) -> ('a1
+        tree -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a1 tree ->
+        (key * 'a1) -> __ -> key -> 'a1 -> __ -> 'a2) -> 'a1 tree -> 'a1 tree
+        -> 'a1 tree -> 'a1 coq_R_merge -> 'a2 **)
+
+    let coq_R_merge_rec f f0 f1 _ _ _ = function
+    | R_merge_0 (x, x0) -> f x x0 __
+    | R_merge_1 (x, x0, x1, x2, x3, x4, x5) -> f0 x x0 x1 x2 x3 x4 x5 __ __
+    | R_merge_2 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12,
+                 x13, x14) ->
+      f1 x x0 x1 x2 x3 x4 x5 __ x6 x7 x8 x9 x10 __ x11 x12 __ x13 x14 __
+
+    type 'elt coq_R_remove =
+    | R_remove_0 of 'elt tree
+    | R_remove_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * 
+       I.t * 'elt tree * 'elt coq_R_remove
+    | R_remove_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+    | R_remove_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * 
+       I.t * 'elt tree * 'elt coq_R_remove
+
+    (** val coq_R_remove_rect :
+        X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1 coq_R_remove
+        -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+        I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1 coq_R_remove
+        -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_remove -> 'a2 **)
+
+    let rec coq_R_remove_rect x f f0 f1 f2 _ _ = function
+    | R_remove_0 m -> f m __
+    | R_remove_1 (m, l, y, d, r0, _x, _res, r1) ->
+      f0 m l y d r0 _x __ __ __ _res r1
+        (coq_R_remove_rect x f f0 f1 f2 l _res r1)
+    | R_remove_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+    | R_remove_3 (m, l, y, d, r0, _x, _res, r1) ->
+      f2 m l y d r0 _x __ __ __ _res r1
+        (coq_R_remove_rect x f f0 f1 f2 r0 _res r1)
+
+    (** val coq_R_remove_rec :
+        X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1 coq_R_remove
+        -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+        I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1 coq_R_remove
+        -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_remove -> 'a2 **)
+
+    let rec coq_R_remove_rec x f f0 f1 f2 _ _ = function
+    | R_remove_0 m -> f m __
+    | R_remove_1 (m, l, y, d, r0, _x, _res, r1) ->
+      f0 m l y d r0 _x __ __ __ _res r1
+        (coq_R_remove_rec x f f0 f1 f2 l _res r1)
+    | R_remove_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+    | R_remove_3 (m, l, y, d, r0, _x, _res, r1) ->
+      f2 m l y d r0 _x __ __ __ _res r1
+        (coq_R_remove_rec x f f0 f1 f2 r0 _res r1)
+
+    type 'elt coq_R_concat =
+    | R_concat_0 of 'elt tree * 'elt tree
+    | R_concat_1 of 'elt tree * 'elt tree * 'elt tree * key * 'elt
+       * 'elt tree * I.t
+    | R_concat_2 of 'elt tree * 'elt tree * 'elt tree * key * 'elt
+       * 'elt tree * I.t * 'elt tree * key * 'elt * 'elt tree * I.t
+       * 'elt tree * (key * 'elt)
+
+    (** val coq_R_concat_rect :
+        ('a1 tree -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> 'a1
+        tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2) -> ('a1
+        tree -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a1 tree ->
+        (key * 'a1) -> __ -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 tree -> 'a1
+        coq_R_concat -> 'a2 **)
+
+    let coq_R_concat_rect f f0 f1 _ _ _ = function
+    | R_concat_0 (x, x0) -> f x x0 __
+    | R_concat_1 (x, x0, x1, x2, x3, x4, x5) -> f0 x x0 x1 x2 x3 x4 x5 __ __
+    | R_concat_2 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+      f1 x x0 x1 x2 x3 x4 x5 __ x6 x7 x8 x9 x10 __ x11 x12 __
+
+    (** val coq_R_concat_rec :
+        ('a1 tree -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> 'a1
+        tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2) -> ('a1
+        tree -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a1 tree ->
+        (key * 'a1) -> __ -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 tree -> 'a1
+        coq_R_concat -> 'a2 **)
+
+    let coq_R_concat_rec f f0 f1 _ _ _ = function
+    | R_concat_0 (x, x0) -> f x x0 __
+    | R_concat_1 (x, x0, x1, x2, x3, x4, x5) -> f0 x x0 x1 x2 x3 x4 x5 __ __
+    | R_concat_2 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+      f1 x x0 x1 x2 x3 x4 x5 __ x6 x7 x8 x9 x10 __ x11 x12 __
+
+    type 'elt coq_R_split =
+    | R_split_0 of 'elt tree
+    | R_split_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+       * 'elt triple * 'elt coq_R_split * 'elt tree * 'elt option * 'elt tree
+    | R_split_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+    | R_split_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+       * 'elt triple * 'elt coq_R_split * 'elt tree * 'elt option * 'elt tree
+
+    (** val coq_R_split_rect :
+        X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 triple -> 'a1 coq_R_split
+        -> 'a2 -> 'a1 tree -> 'a1 option -> 'a1 tree -> __ -> 'a2) -> ('a1
+        tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __
+        -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t ->
+        __ -> __ -> __ -> 'a1 triple -> 'a1 coq_R_split -> 'a2 -> 'a1 tree ->
+        'a1 option -> 'a1 tree -> __ -> 'a2) -> 'a1 tree -> 'a1 triple -> 'a1
+        coq_R_split -> 'a2 **)
+
+    let rec coq_R_split_rect x f f0 f1 f2 _ _ = function
+    | R_split_0 m -> f m __
+    | R_split_1 (m, l, y, d, r0, _x, _res, r1, ll, o, rl) ->
+      f0 m l y d r0 _x __ __ __ _res r1
+        (coq_R_split_rect x f f0 f1 f2 l _res r1) ll o rl __
+    | R_split_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+    | R_split_3 (m, l, y, d, r0, _x, _res, r1, rl, o, rr) ->
+      f2 m l y d r0 _x __ __ __ _res r1
+        (coq_R_split_rect x f f0 f1 f2 r0 _res r1) rl o rr __
+
+    (** val coq_R_split_rec :
+        X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+        -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 triple -> 'a1 coq_R_split
+        -> 'a2 -> 'a1 tree -> 'a1 option -> 'a1 tree -> __ -> 'a2) -> ('a1
+        tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __
+        -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t ->
+        __ -> __ -> __ -> 'a1 triple -> 'a1 coq_R_split -> 'a2 -> 'a1 tree ->
+        'a1 option -> 'a1 tree -> __ -> 'a2) -> 'a1 tree -> 'a1 triple -> 'a1
+        coq_R_split -> 'a2 **)
+
+    let rec coq_R_split_rec x f f0 f1 f2 _ _ = function
+    | R_split_0 m -> f m __
+    | R_split_1 (m, l, y, d, r0, _x, _res, r1, ll, o, rl) ->
+      f0 m l y d r0 _x __ __ __ _res r1
+        (coq_R_split_rec x f f0 f1 f2 l _res r1) ll o rl __
+    | R_split_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+    | R_split_3 (m, l, y, d, r0, _x, _res, r1, rl, o, rr) ->
+      f2 m l y d r0 _x __ __ __ _res r1
+        (coq_R_split_rec x f f0 f1 f2 r0 _res r1) rl o rr __
+
+    type ('elt, 'x) coq_R_map_option =
+    | R_map_option_0 of 'elt tree
+    | R_map_option_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * 
+       I.t * 'x * 'x tree * ('elt, 'x) coq_R_map_option * 'x tree
+       * ('elt, 'x) coq_R_map_option
+    | R_map_option_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * 
+       I.t * 'x tree * ('elt, 'x) coq_R_map_option * 'x tree
+       * ('elt, 'x) coq_R_map_option
+
+    (** val coq_R_map_option_rect :
+        (key -> 'a1 -> 'a2 option) -> ('a1 tree -> __ -> 'a3) -> ('a1 tree ->
+        'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2 -> __ -> 'a2
+        tree -> ('a1, 'a2) coq_R_map_option -> 'a3 -> 'a2 tree -> ('a1, 'a2)
+        coq_R_map_option -> 'a3 -> 'a3) -> ('a1 tree -> 'a1 tree -> key ->
+        'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2 tree -> ('a1, 'a2)
+        coq_R_map_option -> 'a3 -> 'a2 tree -> ('a1, 'a2) coq_R_map_option ->
+        'a3 -> 'a3) -> 'a1 tree -> 'a2 tree -> ('a1, 'a2) coq_R_map_option ->
+        'a3 **)
+
+    let rec coq_R_map_option_rect f f0 f1 f2 _ _ = function
+    | R_map_option_0 m -> f0 m __
+    | R_map_option_1 (m, l, x, d, r0, _x, d', _res0, r1, _res, r2) ->
+      f1 m l x d r0 _x __ d' __ _res0 r1
+        (coq_R_map_option_rect f f0 f1 f2 l _res0 r1) _res r2
+        (coq_R_map_option_rect f f0 f1 f2 r0 _res r2)
+    | R_map_option_2 (m, l, x, d, r0, _x, _res0, r1, _res, r2) ->
+      f2 m l x d r0 _x __ __ _res0 r1
+        (coq_R_map_option_rect f f0 f1 f2 l _res0 r1) _res r2
+        (coq_R_map_option_rect f f0 f1 f2 r0 _res r2)
+
+    (** val coq_R_map_option_rec :
+        (key -> 'a1 -> 'a2 option) -> ('a1 tree -> __ -> 'a3) -> ('a1 tree ->
+        'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2 -> __ -> 'a2
+        tree -> ('a1, 'a2) coq_R_map_option -> 'a3 -> 'a2 tree -> ('a1, 'a2)
+        coq_R_map_option -> 'a3 -> 'a3) -> ('a1 tree -> 'a1 tree -> key ->
+        'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2 tree -> ('a1, 'a2)
+        coq_R_map_option -> 'a3 -> 'a2 tree -> ('a1, 'a2) coq_R_map_option ->
+        'a3 -> 'a3) -> 'a1 tree -> 'a2 tree -> ('a1, 'a2) coq_R_map_option ->
+        'a3 **)
+
+    let rec coq_R_map_option_rec f f0 f1 f2 _ _ = function
+    | R_map_option_0 m -> f0 m __
+    | R_map_option_1 (m, l, x, d, r0, _x, d', _res0, r1, _res, r2) ->
+      f1 m l x d r0 _x __ d' __ _res0 r1
+        (coq_R_map_option_rec f f0 f1 f2 l _res0 r1) _res r2
+        (coq_R_map_option_rec f f0 f1 f2 r0 _res r2)
+    | R_map_option_2 (m, l, x, d, r0, _x, _res0, r1, _res, r2) ->
+      f2 m l x d r0 _x __ __ _res0 r1
+        (coq_R_map_option_rec f f0 f1 f2 l _res0 r1) _res r2
+        (coq_R_map_option_rec f f0 f1 f2 r0 _res r2)
+
+    type ('elt, 'x0, 'x) coq_R_map2_opt =
+    | R_map2_opt_0 of 'elt tree * 'x0 tree
+    | R_map2_opt_1 of 'elt tree * 'x0 tree * 'elt tree * key * 'elt
+       * 'elt tree * I.t
+    | R_map2_opt_2 of 'elt tree * 'x0 tree * 'elt tree * key * 'elt
+       * 'elt tree * I.t * 'x0 tree * key * 'x0 * 'x0 tree * I.t * 'x0 tree
+       * 'x0 option * 'x0 tree * 'x * 'x tree
+       * ('elt, 'x0, 'x) coq_R_map2_opt * 'x tree
+       * ('elt, 'x0, 'x) coq_R_map2_opt
+    | R_map2_opt_3 of 'elt tree * 'x0 tree * 'elt tree * key * 'elt
+       * 'elt tree * I.t * 'x0 tree * key * 'x0 * 'x0 tree * I.t * 'x0 tree
+       * 'x0 option * 'x0 tree * 'x tree * ('elt, 'x0, 'x) coq_R_map2_opt
+       * 'x tree * ('elt, 'x0, 'x) coq_R_map2_opt
+
+    (** val coq_R_map2_opt_rect :
+        (key -> 'a1 -> 'a2 option -> 'a3 option) -> ('a1 tree -> 'a3 tree) ->
+        ('a2 tree -> 'a3 tree) -> ('a1 tree -> 'a2 tree -> __ -> 'a4) -> ('a1
+        tree -> 'a2 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> __ -> 'a4) -> ('a1 tree -> 'a2 tree -> 'a1 tree -> key -> 'a1 ->
+        'a1 tree -> I.t -> __ -> 'a2 tree -> key -> 'a2 -> 'a2 tree -> I.t ->
+        __ -> 'a2 tree -> 'a2 option -> 'a2 tree -> __ -> 'a3 -> __ -> 'a3
+        tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a3 tree -> ('a1,
+        'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a4) -> ('a1 tree -> 'a2 tree ->
+        'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2 tree -> key ->
+        'a2 -> 'a2 tree -> I.t -> __ -> 'a2 tree -> 'a2 option -> 'a2 tree ->
+        __ -> __ -> 'a3 tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a3
+        tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a4) -> 'a1 tree ->
+        'a2 tree -> 'a3 tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 **)
+
+    let rec coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 _ _ _ = function
+    | R_map2_opt_0 (m1, m2) -> f0 m1 m2 __
+    | R_map2_opt_1 (m1, m2, l1, x1, d1, r1, _x) ->
+      f1 m1 m2 l1 x1 d1 r1 _x __ __
+    | R_map2_opt_2 (m1, m2, l1, x1, d1, r1, _x, _x0, _x1, _x2, _x3, _x4, l2',
+                    o2, r2', e, _res0, r0, _res, r2) ->
+      f2 m1 m2 l1 x1 d1 r1 _x __ _x0 _x1 _x2 _x3 _x4 __ l2' o2 r2' __ e __
+        _res0 r0
+        (coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 l1 l2' _res0 r0) _res r2
+        (coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 r1 r2' _res r2)
+    | R_map2_opt_3 (m1, m2, l1, x1, d1, r1, _x, _x0, _x1, _x2, _x3, _x4, l2',
+                    o2, r2', _res0, r0, _res, r2) ->
+      f3 m1 m2 l1 x1 d1 r1 _x __ _x0 _x1 _x2 _x3 _x4 __ l2' o2 r2' __ __
+        _res0 r0
+        (coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 l1 l2' _res0 r0) _res r2
+        (coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 r1 r2' _res r2)
+
+    (** val coq_R_map2_opt_rec :
+        (key -> 'a1 -> 'a2 option -> 'a3 option) -> ('a1 tree -> 'a3 tree) ->
+        ('a2 tree -> 'a3 tree) -> ('a1 tree -> 'a2 tree -> __ -> 'a4) -> ('a1
+        tree -> 'a2 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+        -> __ -> 'a4) -> ('a1 tree -> 'a2 tree -> 'a1 tree -> key -> 'a1 ->
+        'a1 tree -> I.t -> __ -> 'a2 tree -> key -> 'a2 -> 'a2 tree -> I.t ->
+        __ -> 'a2 tree -> 'a2 option -> 'a2 tree -> __ -> 'a3 -> __ -> 'a3
+        tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a3 tree -> ('a1,
+        'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a4) -> ('a1 tree -> 'a2 tree ->
+        'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2 tree -> key ->
+        'a2 -> 'a2 tree -> I.t -> __ -> 'a2 tree -> 'a2 option -> 'a2 tree ->
+        __ -> __ -> 'a3 tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a3
+        tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a4) -> 'a1 tree ->
+        'a2 tree -> 'a3 tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 **)
+
+    let rec coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 _ _ _ = function
+    | R_map2_opt_0 (m1, m2) -> f0 m1 m2 __
+    | R_map2_opt_1 (m1, m2, l1, x1, d1, r1, _x) ->
+      f1 m1 m2 l1 x1 d1 r1 _x __ __
+    | R_map2_opt_2 (m1, m2, l1, x1, d1, r1, _x, _x0, _x1, _x2, _x3, _x4, l2',
+                    o2, r2', e, _res0, r0, _res, r2) ->
+      f2 m1 m2 l1 x1 d1 r1 _x __ _x0 _x1 _x2 _x3 _x4 __ l2' o2 r2' __ e __
+        _res0 r0 (coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 l1 l2' _res0 r0)
+        _res r2 (coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 r1 r2' _res r2)
+    | R_map2_opt_3 (m1, m2, l1, x1, d1, r1, _x, _x0, _x1, _x2, _x3, _x4, l2',
+                    o2, r2', _res0, r0, _res, r2) ->
+      f3 m1 m2 l1 x1 d1 r1 _x __ _x0 _x1 _x2 _x3 _x4 __ l2' o2 r2' __ __
+        _res0 r0 (coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 l1 l2' _res0 r0)
+        _res r2 (coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 r1 r2' _res r2)
+
+    (** val fold' : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 tree -> 'a2 -> 'a2 **)
+
+    let fold' f s =
+      L.fold f (elements s)
+
+    (** val flatten_e : 'a1 enumeration -> (key * 'a1) list **)
+
+    let rec flatten_e = function
+    | End -> Nil
+    | More (x, e0, t0, r) -> Cons ((x, e0), (app (elements t0) (flatten_e r)))
+   end
+ end
+
+module IntMake =
+ functor (I:Int) ->
+ functor (X:OrderedType) ->
+ struct
+  module E = X
+
+  module Raw = Coq_Raw(I)(X)
+
+  type 'elt bst =
+    'elt Raw.tree
+    (* singleton inductive, whose constructor was Bst *)
+
+  (** val this : 'a1 bst -> 'a1 Raw.tree **)
+
+  let this b =
+    b
+
+  type 'elt t = 'elt bst
+
+  type key = E.t
+
+  (** val empty : 'a1 t **)
+
+  let empty =
+    Raw.empty
+
+  (** val is_empty : 'a1 t -> bool **)
+
+  let is_empty m =
+    Raw.is_empty (this m)
+
+  (** val add : key -> 'a1 -> 'a1 t -> 'a1 t **)
+
+  let add x e m =
+    Raw.add x e (this m)
+
+  (** val remove : key -> 'a1 t -> 'a1 t **)
+
+  let remove x m =
+    Raw.remove x (this m)
+
+  (** val mem : key -> 'a1 t -> bool **)
+
+  let mem x m =
+    Raw.mem x (this m)
+
+  (** val find : key -> 'a1 t -> 'a1 option **)
+
+  let find x m =
+    Raw.find x (this m)
+
+  (** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+
+  let map f m =
+    Raw.map f (this m)
+
+  (** val mapi : (key -> 'a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+
+  let mapi f m =
+    Raw.mapi f (this m)
+
+  (** val map2 :
+      ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t -> 'a3 t **)
+
+  let map2 f m m' =
+    Raw.map2 f (this m) (this m')
+
+  (** val elements : 'a1 t -> (key * 'a1) list **)
+
+  let elements m =
+    Raw.elements (this m)
+
+  (** val cardinal : 'a1 t -> nat **)
+
+  let cardinal m =
+    Raw.cardinal (this m)
+
+  (** val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2 **)
+
+  let fold f m i =
+    Raw.fold f (this m) i
+
+  (** val equal : ('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool **)
+
+  let equal cmp m m' =
+    Raw.equal cmp (this m) (this m')
+ end
+
+module Make =
+ functor (X:OrderedType) ->
+ IntMake(Z_as_Int)(X)
+
+module IntOrderedType =
+ struct
+  type t = Uint63.t
+
+  (** val compare : Uint63.t -> Uint63.t -> Uint63.t compare1 **)
+
+  let compare x y =
+    if ltb0 x y then LT else if eqb0 x y then EQ else GT
+
+  (** val eq_dec : Uint63.t -> Uint63.t -> sumbool **)
+
+  let eq_dec x y =
+    if eqb0 x y then Left else Right
+ end
+
+module Map = Make(IntOrderedType)
+
+type 'a array = ('a Map.t * 'a) * Uint63.t
+
+(** val make : Uint63.t -> 'a1 -> 'a1 array **)
+
+let make l d =
+  ((Map.empty, d), l)
+
+module Coq__1 = struct
+ (** val get : 'a1 array -> Uint63.t -> 'a1 **)
+ let get t0 i =
+   let (td, l) = t0 in
+   let (t1, d) = td in
+   if ltb0 i l then (match Map.find i t1 with
+                     | Some x -> x
+                     | None -> d) else d
+end
+include Coq__1
+
+(** val set : 'a1 array -> Uint63.t -> 'a1 -> 'a1 array **)
+
+let set t0 i a =
+  let (td, l) = t0 in
+  if leb0 l i then t0 else let (t1, d) = td in (((Map.add i a t1), d), l)
+
+(** val length : 'a1 array -> Uint63.t **)
+
+let length = function
+| (_, l) -> l
+
+(** val iter_int63_aux : nat -> Uint63.t -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
+
+let rec iter_int63_aux n i f =
+  match n with
+  | O -> (fun x -> x)
+  | S n0 ->
+    if eqb0 i (Uint63.of_int (0))
+    then (fun x -> x)
+    else let g = iter_int63_aux n0 (lsr0 i (Uint63.of_int (1))) f in
+         (fun x -> if bit i (Uint63.of_int (0)) then f (g (g x)) else g (g x))
+
+(** val iter_int63 : Uint63.t -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
+
+let iter_int63 i f x =
+  iter_int63_aux size i f x
+
+(** val foldi :
+    (Uint63.t -> 'a1 -> 'a1) -> Uint63.t -> Uint63.t -> 'a1 -> 'a1 **)
+
+let foldi f from to0 a =
+  if leb0 to0 from
+  then a
+  else let (_, r) =
+         iter_int63 (sub0 to0 from) (fun jy ->
+           let (j, y) = jy in ((add0 j (Uint63.of_int (1))), (f j y))) (from,
+           a)
+       in
+       r
+
+(** val to_list : 'a1 array -> 'a1 list **)
+
+let to_list t0 =
+  rev
+    (foldi (fun i l -> Cons ((get t0 i), l)) (Uint63.of_int (0)) (length t0)
+      Nil)
+
+module Lit =
+ struct
+  (** val _true : Uint63.t **)
+
   let _true =
-    (ExtrNative.of_uint(0))
-  
-  (** val _false : int **)
-  
-  let _false =
-    (ExtrNative.of_uint(2))
-  
-  (** val eqb : int -> int -> bool **)
-  
-  let eqb l l' =
-    eqb l l'
-  
-  (** val interp : Valuation.t -> int -> bool **)
-  
-  let interp rho l =
-    if is_pos l
-    then Var.interp rho (blit l)
-    else negb (Var.interp rho (blit l))
+    (Uint63.of_int (0))
  end
 
-module C = 
- struct 
-  type t = int list
-  
-  (** val interp : Valuation.t -> t -> bool **)
-  
-  let interp rho l =
-    existsb (Lit.interp rho) l
-  
+module C =
+ struct
+  type t = Uint63.t list
+
   (** val _true : t **)
-  
+
   let _true =
     Cons (Lit._true, Nil)
-  
+
   (** val is_false : t -> bool **)
-  
+
   let is_false = function
   | Nil -> true
-  | Cons (i, l) -> false
-  
-  (** val or_aux : (t -> t -> t) -> int -> t -> t -> int list **)
-  
+  | Cons (_, _) -> false
+
+  (** val or_aux : (t -> t -> t) -> Uint63.t -> t -> t -> Uint63.t list **)
+
   let rec or_aux or0 l1 c1 c2 = match c2 with
   | Nil -> Cons (l1, c1)
   | Cons (l2, c2') ->
-    (match compare l1 l2 with
-     | ExtrNative.Eq -> Cons (l1, (or0 c1 c2'))
-     | ExtrNative.Lt -> Cons (l1, (or0 c1 c2))
-     | ExtrNative.Gt -> Cons (l2, (or_aux or0 l1 c1 c2')))
-  
+    (match compare0 l1 l2 with
+     | 0 -> Cons (l1, (or0 c1 c2'))
+     | (-1) -> Cons (l1, (or0 c1 c2))
+     | 1 -> Cons (l2, (or_aux or0 l1 c1 c2')))
+
   (** val coq_or : t -> t -> t **)
-  
+
   let rec coq_or c1 c2 =
     match c1 with
     | Nil -> c2
@@ -249,29 +2409,29 @@ module C =
       (match c2 with
        | Nil -> c1
        | Cons (l2, c2') ->
-         (match compare l1 l2 with
-          | ExtrNative.Eq -> Cons (l1, (coq_or c3 c2'))
-          | ExtrNative.Lt -> Cons (l1, (coq_or c3 c2))
-          | ExtrNative.Gt -> Cons (l2, (or_aux coq_or l1 c3 c2'))))
-  
-  (** val resolve_aux : (t -> t -> t) -> int -> t -> t -> t **)
-  
+         (match compare0 l1 l2 with
+          | 0 -> Cons (l1, (coq_or c3 c2'))
+          | (-1) -> Cons (l1, (coq_or c3 c2))
+          | 1 -> Cons (l2, (or_aux coq_or l1 c3 c2'))))
+
+  (** val resolve_aux : (t -> t -> t) -> Uint63.t -> t -> t -> t **)
+
   let rec resolve_aux resolve0 l1 c1 c2 = match c2 with
   | Nil -> _true
   | Cons (l2, c2') ->
-    (match compare l1 l2 with
-     | ExtrNative.Eq -> Cons (l1, (resolve0 c1 c2'))
-     | ExtrNative.Lt ->
-       if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+    (match compare0 l1 l2 with
+     | 0 -> Cons (l1, (resolve0 c1 c2'))
+     | (-1) ->
+       if eqb0 (lxor0 l1 l2) (Uint63.of_int (1))
        then coq_or c1 c2'
        else Cons (l1, (resolve0 c1 c2))
-     | ExtrNative.Gt ->
-       if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+     | 1 ->
+       if eqb0 (lxor0 l1 l2) (Uint63.of_int (1))
        then coq_or c1 c2'
        else Cons (l2, (resolve_aux resolve0 l1 c1 c2')))
-  
+
   (** val resolve : t -> t -> t **)
-  
+
   let rec resolve c1 c2 =
     match c1 with
     | Nil -> _true
@@ -279,165 +2439,107 @@ module C =
       (match c2 with
        | Nil -> _true
        | Cons (l2, c2') ->
-         (match compare l1 l2 with
-          | ExtrNative.Eq -> Cons (l1, (resolve c3 c2'))
-          | ExtrNative.Lt ->
-            if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+         (match compare0 l1 l2 with
+          | 0 -> Cons (l1, (resolve c3 c2'))
+          | (-1) ->
+            if eqb0 (lxor0 l1 l2) (Uint63.of_int (1))
             then coq_or c3 c2'
             else Cons (l1, (resolve c3 c2))
-          | ExtrNative.Gt ->
-            if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+          | 1 ->
+            if eqb0 (lxor0 l1 l2) (Uint63.of_int (1))
             then coq_or c3 c2'
             else Cons (l2, (resolve_aux resolve l1 c3 c2'))))
  end
 
-module S = 
- struct 
+module S =
+ struct
   type t = C.t array
-  
-  (** val get : t -> int -> C.t **)
-  
-  let get s cid =
-    get s cid
-  
-  (** val internal_set : t -> int -> C.t -> t **)
-  
-  let internal_set s cid c =
-    set s cid c
-  
-  (** val make : int -> t **)
-  
+
+  (** val get : t -> Uint63.t -> C.t **)
+
+  let get =
+    get
+
+  (** val internal_set : t -> Uint63.t -> C.t -> t **)
+
+  let internal_set =
+    set
+
+  (** val make : Uint63.t -> t **)
+
   let make nclauses =
     make nclauses C._true
-  
-  (** val insert : int -> int list -> int list **)
-  
-  let rec insert l1 c = match c with
+
+  (** val insert_no_simpl : Uint63.t -> Uint63.t list -> Uint63.t list **)
+
+  let rec insert_no_simpl l1 c = match c with
   | Nil -> Cons (l1, Nil)
   | Cons (l2, c') ->
-    (match compare l1 l2 with
-     | ExtrNative.Eq -> c
-     | ExtrNative.Lt ->
-       if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
-       then C._true
-       else Cons (l1, c)
-     | ExtrNative.Gt ->
-       if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
-       then C._true
-       else Cons (l2, (insert l1 c')))
-  
-  (** val sort_uniq : int list -> int list **)
-  
-  let rec sort_uniq = function
+    (match compare0 l1 l2 with
+     | 0 -> c
+     | (-1) -> Cons (l1, c)
+     | 1 -> Cons (l2, (insert_no_simpl l1 c')))
+
+  (** val sort : Uint63.t list -> Uint63.t list **)
+
+  let rec sort = function
   | Nil -> Nil
-  | Cons (l1, c0) -> insert l1 (sort_uniq c0)
-  
-  (** val set_clause : t -> int -> C.t -> t **)
-  
+  | Cons (l1, c0) -> insert_no_simpl l1 (sort c0)
+
+  (** val set_clause : t -> Uint63.t -> C.t -> t **)
+
   let set_clause s pos c =
-    set s pos (sort_uniq c)
-  
-  (** val set_resolve : t -> int -> int array -> t **)
-  
+    set s pos (sort c)
+
+  (** val set_resolve : t -> Uint63.t -> Uint63.t array -> t **)
+
   let set_resolve s pos r =
     let len = length r in
-    if eqb len (ExtrNative.of_uint(0))
+    if eqb0 len (Uint63.of_int (0))
     then s
     else let c =
-           foldi (fun i c -> C.resolve (get s (Coq__1.get r i)) c)
-             (ExtrNative.of_uint(1)) (sub len (ExtrNative.of_uint(1)))
-             (get s (Coq__1.get r (ExtrNative.of_uint(0))))
+           foldi (fun i c' -> C.resolve (get s (Coq__1.get r i)) c')
+             (Uint63.of_int (1)) len
+             (get s (Coq__1.get r (Uint63.of_int (0))))
          in
          internal_set s pos c
  end
 
-(** val afold_left :
-    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a1) -> 'a2 array -> 'a1 **)
-
-let afold_left default oP f v =
-  let n = length v in
-  if eqb n (ExtrNative.of_uint(0))
-  then default
-  else foldi (fun i a -> oP a (f (get v i))) (ExtrNative.of_uint(1))
-         (sub n (ExtrNative.of_uint(1))) (f (get v (ExtrNative.of_uint(0))))
-
-type 'step _trace_ = 'step array array
+type 'step _trace_ = 'step list * 'step
 
 (** val _checker_ :
-    (S.t -> 'a1 -> S.t) -> (C.t -> bool) -> S.t -> 'a1 _trace_ -> int -> bool **)
+    (S.t -> 'a1 -> S.t) -> (C.t -> bool) -> S.t -> 'a1 _trace_ -> Uint63.t ->
+    bool **)
 
 let _checker_ check_step is_false0 s t0 confl =
-  let s' = fold_left (fun s0 a -> fold_left check_step s0 a) s t0 in
-  is_false0 (S.get s' confl)
+  let s' = fold_left check_step (fst t0) s in is_false0 (S.get s' confl)
 
-module Sat_Checker = 
- struct 
+module Sat_Checker =
+ struct
   type step =
-  | Res of int * int array
-  
-  (** val step_rect : (int -> int array -> 'a1) -> step -> 'a1 **)
-  
-  let step_rect f = function
-  | Res (x, x0) -> f x x0
-  
-  (** val step_rec : (int -> int array -> 'a1) -> step -> 'a1 **)
-  
-  let step_rec f = function
-  | Res (x, x0) -> f x x0
-  
+  | Res of Uint63.t * Uint63.t array
+
   (** val resolution_checker :
-      (C.t -> bool) -> S.t -> step _trace_ -> int -> bool **)
-  
+      (C.t -> bool) -> S.t -> step _trace_ -> Uint63.t -> bool **)
+
   let resolution_checker s t0 =
     _checker_ (fun s0 st -> let Res (pos, r) = st in S.set_resolve s0 pos r)
       s t0
-  
-  type dimacs = int array array
-  
-  (** val coq_C_interp_or : Valuation.t -> int array -> bool **)
-  
-  let coq_C_interp_or rho c =
-    afold_left false (fun b1 b2 -> if b1 then true else b2) (Lit.interp rho)
-      c
-  
-  (** val valid : Valuation.t -> dimacs -> bool **)
-  
-  let valid rho d =
-    afold_left true (fun b1 b2 -> if b1 then b2 else false)
-      (coq_C_interp_or rho) d
-  
+
+  type dimacs = Uint63.t array array
+
   type certif =
-  | Certif of int * step _trace_ * int
-  
-  (** val certif_rect :
-      (int -> step _trace_ -> int -> 'a1) -> certif -> 'a1 **)
-  
-  let certif_rect f = function
-  | Certif (x, x0, x1) -> f x x0 x1
-  
-  (** val certif_rec :
-      (int -> step _trace_ -> int -> 'a1) -> certif -> 'a1 **)
-  
-  let certif_rec f = function
-  | Certif (x, x0, x1) -> f x x0 x1
-  
+  | Certif of Uint63.t * step _trace_ * Uint63.t
+
   (** val add_roots : S.t -> dimacs -> S.t **)
-  
+
   let add_roots s d =
-    foldi_right (fun i c s0 -> S.set_clause s0 i (to_list c)) d s
-  
+    foldi (fun i s0 -> S.set_clause s0 i (to_list (get d i)))
+      (Uint63.of_int (0)) (length d) s
+
   (** val checker : dimacs -> certif -> bool **)
-  
+
   let checker d = function
   | Certif (nclauses, t0, confl_id) ->
     resolution_checker C.is_false (add_roots (S.make nclauses) d) t0 confl_id
-  
-  (** val interp_var : (int -> bool) -> int -> bool **)
-  
-  let interp_var rho x =
-    match compare x (ExtrNative.of_uint(1)) with
-    | ExtrNative.Eq -> false
-    | ExtrNative.Lt -> true
-    | ExtrNative.Gt -> rho (sub x (ExtrNative.of_uint(1)))
  end
-
-- 
cgit