open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Jmeq

open Russell

type dAEMONXXX =
| K1DAEMONXXX
| K2DAEMONXXX

(** val dAEMONXXX_rect_Type4 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
let rec dAEMONXXX_rect_Type4 h_K1DAEMONXXX h_K2DAEMONXXX = function
| K1DAEMONXXX -> h_K1DAEMONXXX
| K2DAEMONXXX -> h_K2DAEMONXXX

(** val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
let rec dAEMONXXX_rect_Type5 h_K1DAEMONXXX h_K2DAEMONXXX = function
| K1DAEMONXXX -> h_K1DAEMONXXX
| K2DAEMONXXX -> h_K2DAEMONXXX

(** val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
let rec dAEMONXXX_rect_Type3 h_K1DAEMONXXX h_K2DAEMONXXX = function
| K1DAEMONXXX -> h_K1DAEMONXXX
| K2DAEMONXXX -> h_K2DAEMONXXX

(** val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
let rec dAEMONXXX_rect_Type2 h_K1DAEMONXXX h_K2DAEMONXXX = function
| K1DAEMONXXX -> h_K1DAEMONXXX
| K2DAEMONXXX -> h_K2DAEMONXXX

(** val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
let rec dAEMONXXX_rect_Type1 h_K1DAEMONXXX h_K2DAEMONXXX = function
| K1DAEMONXXX -> h_K1DAEMONXXX
| K2DAEMONXXX -> h_K2DAEMONXXX

(** val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
let rec dAEMONXXX_rect_Type0 h_K1DAEMONXXX h_K2DAEMONXXX = function
| K1DAEMONXXX -> h_K1DAEMONXXX
| K2DAEMONXXX -> h_K2DAEMONXXX

(** val dAEMONXXX_inv_rect_Type4 :
    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let dAEMONXXX_inv_rect_Type4 hterm h1 h2 =
  let hcut = dAEMONXXX_rect_Type4 h1 h2 hterm in hcut __

(** val dAEMONXXX_inv_rect_Type3 :
    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let dAEMONXXX_inv_rect_Type3 hterm h1 h2 =
  let hcut = dAEMONXXX_rect_Type3 h1 h2 hterm in hcut __

(** val dAEMONXXX_inv_rect_Type2 :
    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let dAEMONXXX_inv_rect_Type2 hterm h1 h2 =
  let hcut = dAEMONXXX_rect_Type2 h1 h2 hterm in hcut __

(** val dAEMONXXX_inv_rect_Type1 :
    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let dAEMONXXX_inv_rect_Type1 hterm h1 h2 =
  let hcut = dAEMONXXX_rect_Type1 h1 h2 hterm in hcut __

(** val dAEMONXXX_inv_rect_Type0 :
    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let dAEMONXXX_inv_rect_Type0 hterm h1 h2 =
  let hcut = dAEMONXXX_rect_Type0 h1 h2 hterm in hcut __

(** val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __ **)
let dAEMONXXX_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
     | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y

(** val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __ **)
let dAEMONXXX_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
     | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y

(** val ltb : Nat.nat -> Nat.nat -> Bool.bool **)
let ltb m n =
  Nat.leb (Nat.S m) n

(** val geb : Nat.nat -> Nat.nat -> Bool.bool **)
let geb m n =
  Nat.leb n m

(** val gtb : Nat.nat -> Nat.nat -> Bool.bool **)
let gtb m n =
  ltb n m

(** val eq_nat : Nat.nat -> Nat.nat -> Bool.bool **)
let rec eq_nat n m =
  match n with
  | Nat.O ->
    (match m with
     | Nat.O -> Bool.True
     | Nat.S x -> Bool.False)
  | Nat.S n' ->
    (match m with
     | Nat.O -> Bool.False
     | Nat.S m' -> eq_nat n' m')

(** val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
let rec forall f = function
| List.Nil -> Bool.True
| List.Cons (hd, tl) -> Bool.andb (f hd) (forall f tl)

(** val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
let rec prefix k = function
| List.Nil -> List.Nil
| List.Cons (hd, tl) ->
  (match k with
   | Nat.O -> List.Nil
   | Nat.S k' -> List.Cons (hd, (prefix k' tl)))

(** val fold_left2 :
    ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list ->
    'a1 **)
let rec fold_left2 f accu left right =
  (match left with
   | List.Nil ->
     (fun _ ->
       (match right with
        | List.Nil -> (fun _ -> accu)
        | List.Cons (hd, tl) ->
          (fun _ ->
            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
   | List.Cons (hd, tl) ->
     (fun _ ->
       (match right with
        | List.Nil ->
          (fun _ ->
            Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
        | List.Cons (hd', tl') ->
          (fun _ -> fold_left2 f (f accu hd hd') tl tl')) __)) __

(** val remove_n_first_internal :
    Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
let rec remove_n_first_internal i l n =
  match l with
  | List.Nil -> List.Nil
  | List.Cons (hd, tl) ->
    (match eq_nat i n with
     | Bool.True -> l
     | Bool.False -> remove_n_first_internal (Nat.S i) tl n)

(** val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
let remove_n_first n l =
  remove_n_first_internal Nat.O l n

(** val foldi_from_until_internal :
    Nat.nat -> 'a1 List.list -> 'a1 List.list -> Nat.nat -> (Nat.nat -> 'a1
    List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list **)
let rec foldi_from_until_internal i res rem m f =
  match rem with
  | List.Nil -> res
  | List.Cons (e, tl) ->
    (match geb i m with
     | Bool.True -> res
     | Bool.False -> foldi_from_until_internal (Nat.S i) (f i res e) tl m f)

(** val foldi_from_until :
    Nat.nat -> Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list)
    -> 'a1 List.list -> 'a1 List.list -> 'a1 List.list **)
let foldi_from_until n m f a l =
  foldi_from_until_internal Nat.O a (remove_n_first n l) m f

(** val foldi_from :
    Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
    List.list -> 'a1 List.list -> 'a1 List.list **)
let foldi_from n f a l =
  foldi_from_until n (List.length l) f a l

(** val foldi_until :
    Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
    List.list -> 'a1 List.list -> 'a1 List.list **)
let foldi_until m f a l =
  foldi_from_until Nat.O m f a l

(** val foldi :
    (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list ->
    'a1 List.list -> 'a1 List.list **)
let foldi f a l =
  foldi_from_until Nat.O (List.length l) f a l

(** val hd_safe : 'a1 List.list -> 'a1 **)
let hd_safe l =
  (match l with
   | List.Nil -> (fun _ -> assert false (* absurd case *))
   | List.Cons (hd, tl) -> (fun _ -> hd)) __

(** val tail_safe : 'a1 List.list -> 'a1 List.list **)
let tail_safe l =
  (match l with
   | List.Nil -> (fun _ -> assert false (* absurd case *))
   | List.Cons (hd, tl) -> (fun _ -> tl)) __

(** val safe_split :
    'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod **)
let rec safe_split l index =
  (match index with
   | Nat.O -> (fun _ -> { Types.fst = List.Nil; Types.snd = l })
   | Nat.S index' ->
     (fun _ ->
       (match l with
        | List.Nil -> (fun _ -> assert false (* absurd case *))
        | List.Cons (hd, tl) ->
          (fun _ ->
            let { Types.fst = l1; Types.snd = l2 } = safe_split tl index' in
            { Types.fst = (List.Cons (hd, l1)); Types.snd = l2 })) __)) __

(** val nth_safe : Nat.nat -> 'a1 List.list -> 'a1 **)
let rec nth_safe index the_list =
  (match index with
   | Nat.O ->
     (match the_list with
      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
      | List.Cons (hd, tl) -> (fun _ -> hd))
   | Nat.S index' ->
     (match the_list with
      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
      | List.Cons (hd, tl) -> (fun _ -> nth_safe index' tl))) __

(** val last_safe : 'a1 List.list -> 'a1 **)
let last_safe the_list =
  nth_safe (Nat.minus (List.length the_list) (Nat.S Nat.O)) the_list

(** val reduce :
    'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
    Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod **)
let rec reduce left right =
  match left with
  | List.Nil ->
    { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil }; Types.snd =
      { Types.fst = List.Nil; Types.snd = right } }
  | List.Cons (hd, tl) ->
    (match right with
     | List.Nil ->
       { Types.fst = { Types.fst = List.Nil; Types.snd = left }; Types.snd =
         { Types.fst = List.Nil; Types.snd = List.Nil } }
     | List.Cons (hd', tl') ->
       let { Types.fst = cleft; Types.snd = cright } = reduce tl tl' in
       let { Types.fst = commonl; Types.snd = restl } = cleft in
       let { Types.fst = commonr; Types.snd = restr } = cright in
       { Types.fst = { Types.fst = (List.Cons (hd, commonl)); Types.snd =
       restl }; Types.snd = { Types.fst = (List.Cons (hd', commonr));
       Types.snd = restr } })

(** val reduce_strong :
    'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
    Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
    Types.sig0 **)
let rec reduce_strong left right =
  (match left with
   | List.Nil ->
     (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil };
       Types.snd = { Types.fst = List.Nil; Types.snd = right } })
   | List.Cons (hd, tl) ->
     (fun _ ->
       (match right with
        | List.Nil ->
          (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = left };
            Types.snd = { Types.fst = List.Nil; Types.snd = List.Nil } })
        | List.Cons (hd', tl') ->
          (fun _ ->
            (let { Types.fst = cleft; Types.snd = cright } =
               Types.pi1 (reduce_strong tl tl')
             in
            (fun _ ->
            (let { Types.fst = commonl; Types.snd = restl } = cleft in
            (fun _ ->
            (let { Types.fst = commonr; Types.snd = restr } = cright in
            (fun _ -> { Types.fst = { Types.fst = (List.Cons (hd, commonl));
            Types.snd = restl }; Types.snd = { Types.fst = (List.Cons (hd',
            commonr)); Types.snd = restr } })) __)) __)) __)) __)) __

(** val map2_opt :
    ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
    Types.option **)
let rec map2_opt f left right =
  match left with
  | List.Nil ->
    (match right with
     | List.Nil -> Types.Some List.Nil
     | List.Cons (x, x0) -> Types.None)
  | List.Cons (hd, tl) ->
    (match right with
     | List.Nil -> Types.None
     | List.Cons (hd', tl') ->
       (match map2_opt f tl tl' with
        | Types.None -> Types.None
        | Types.Some tail -> Types.Some (List.Cons ((f hd hd'), tail))))

(** val map2 :
    ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list **)
let rec map2 f left right =
  (match left with
   | List.Nil ->
     (match right with
      | List.Nil -> (fun _ -> List.Nil)
      | List.Cons (x, x0) ->
        (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length x0)) __))
   | List.Cons (hd, tl) ->
     (match right with
      | List.Nil ->
        (fun _ -> Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
      | List.Cons (hd', tl') ->
        (fun _ -> List.Cons ((f hd hd'), (map2 f tl tl'))))) __

(** val map3 :
    ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
    List.list -> 'a4 List.list **)
let rec map3 f left centre right =
  (match left with
   | List.Nil ->
     (fun _ ->
       (match centre with
        | List.Nil ->
          (fun _ ->
            (match right with
             | List.Nil -> (fun _ -> List.Nil)
             | List.Cons (hd, tl) ->
               (fun _ ->
                 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __))
              __)
        | List.Cons (hd, tl) ->
          (fun _ ->
            Logic.eq_rect_Type0 (List.length centre)
              (Logic.eq_rect_Type0 (List.length List.Nil) (fun _ ->
                Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
                (List.length centre)) (List.length right) __)) __)
   | List.Cons (hd, tl) ->
     (fun _ ->
       (match centre with
        | List.Nil ->
          (fun _ ->
            Logic.eq_rect_Type0 (List.length centre)
              (Logic.eq_rect_Type0 (List.length (List.Cons (hd, tl)))
                (fun _ ->
                Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)
                (List.length centre)) (List.length right) __)
        | List.Cons (hd', tl') ->
          (fun _ ->
            (match right with
             | List.Nil ->
               (fun _ _ ->
                 Obj.magic Nat.nat_discr (Nat.S (List.length tl')) Nat.O __)
             | List.Cons (hd'', tl'') ->
               (fun _ _ -> List.Cons ((f hd hd' hd''), (map3 f tl tl' tl''))))
              __ __)) __)) __

(** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let eq_rect_Type0_r a h x =
  (fun _ auto -> auto) __ h

(** val safe_nth : Nat.nat -> 'a1 List.list -> 'a1 **)
let rec safe_nth n l =
  (match n with
   | Nat.O ->
     (match l with
      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
      | List.Cons (hd, tl) -> (fun _ -> hd))
   | Nat.S n' ->
     (match l with
      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
      | List.Cons (hd, tl) -> (fun _ -> safe_nth n' tl))) __

(** val nub_by_internal :
    ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
let rec nub_by_internal f l = function
| Nat.O ->
  (match l with
   | List.Nil -> List.Nil
   | List.Cons (hd, tl) -> l)
| Nat.S n0 ->
  (match l with
   | List.Nil -> List.Nil
   | List.Cons (hd, tl) ->
     List.Cons (hd,
       (nub_by_internal f (List.filter (fun y -> Bool.notb (f y hd)) tl) n0)))

(** val nub_by :
    ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
let nub_by f l =
  nub_by_internal f l (List.length l)

(** val member :
    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool **)
let rec member eq a = function
| List.Nil -> Bool.False
| List.Cons (hd, tl) -> Bool.orb (eq a hd) (member eq a tl)

(** val take : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
let rec take n l =
  match n with
  | Nat.O -> List.Nil
  | Nat.S n0 ->
    (match l with
     | List.Nil -> List.Nil
     | List.Cons (hd, tl) -> List.Cons (hd, (take n0 tl)))

(** val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
let rec drop n l =
  match n with
  | Nat.O -> l
  | Nat.S n0 ->
    (match l with
     | List.Nil -> List.Nil
     | List.Cons (hd, tl) -> drop n0 tl)

(** val list_split :
    Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod **)
let list_split n l =
  { Types.fst = (take n l); Types.snd = (drop n l) }

(** val mapi_internal :
    Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
let rec mapi_internal n f = function
| List.Nil -> List.Nil
| List.Cons (hd, tl) ->
  List.Cons ((f n hd), (mapi_internal (Nat.plus n (Nat.S Nat.O)) f tl))

(** val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
let mapi f l =
  mapi_internal Nat.O f l

(** val zip_pottier :
    'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
let rec zip_pottier left right =
  match left with
  | List.Nil -> List.Nil
  | List.Cons (hd, tl) ->
    (match right with
     | List.Nil -> List.Nil
     | List.Cons (hd', tl') ->
       List.Cons ({ Types.fst = hd; Types.snd = hd' }, (zip_pottier tl tl')))

(** val zip_safe :
    'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
let rec zip_safe left right =
  (match left with
   | List.Nil ->
     (fun _ ->
       (match right with
        | List.Nil -> (fun _ -> List.Nil)
        | List.Cons (hd, tl) ->
          (fun _ ->
            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
   | List.Cons (hd, tl) ->
     (fun _ ->
       (match right with
        | List.Nil ->
          (fun _ ->
            Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
        | List.Cons (hd', tl') ->
          (fun _ -> List.Cons ({ Types.fst = hd; Types.snd = hd' },
            (zip_safe tl tl')))) __)) __

(** val zip :
    'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
    Types.option **)
let rec zip l r =
  match l with
  | List.Nil -> Types.Some List.Nil
  | List.Cons (hd, tl) ->
    (match r with
     | List.Nil -> Types.None
     | List.Cons (hd', tl') ->
       (match zip tl tl' with
        | Types.None -> Types.None
        | Types.Some tail ->
          Types.Some (List.Cons ({ Types.fst = hd; Types.snd = hd' }, tail))))

(** val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
let rec foldl f a = function
| List.Nil -> a
| List.Cons (hd, tl) -> foldl f (f a hd) tl

(** val rev : 'a1 List.list -> 'a1 List.list **)
let rev l =
  List.reverse l

(** val fold_left_i_aux :
    (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1 **)
let rec fold_left_i_aux f x i = function
| List.Nil -> x
| List.Cons (hd, tl) -> fold_left_i_aux f (f i x hd) (Nat.S i) tl

(** val fold_left_i :
    (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
let fold_left_i f x =
  fold_left_i_aux f x Nat.O

(** val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2 **)
let function_apply f a =
  f a

(** val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1 **)
let rec iterate f a = function
| Nat.O -> a
| Nat.S o -> f (iterate f a o)

(** val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
let rec division_aux m n p =
  match ltb n (Nat.S p) with
  | Bool.True -> Nat.O
  | Bool.False ->
    (match m with
     | Nat.O -> Nat.O
     | Nat.S q -> Nat.S (division_aux q (Nat.minus n (Nat.S p)) p))

(** val division : Nat.nat -> Nat.nat -> Nat.nat **)
let division m = function
| Nat.O -> Nat.S m
| Nat.S o -> division_aux m m o

(** val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
let rec modulus_aux m n p =
  match Nat.leb n p with
  | Bool.True -> n
  | Bool.False ->
    (match m with
     | Nat.O -> n
     | Nat.S o -> modulus_aux o (Nat.minus n (Nat.S p)) p)

(** val modulus : Nat.nat -> Nat.nat -> Nat.nat **)
let modulus m = function
| Nat.O -> m
| Nat.S o -> modulus_aux m m o

(** val divide_with_remainder :
    Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod **)
let divide_with_remainder m n =
  { Types.fst = (division m n); Types.snd = (modulus m n) }

(** val less_than_or_equal_b_elim :
    Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let less_than_or_equal_b_elim m n h1 h2 =
  (match Nat.leb m n with
   | Bool.True -> (fun _ _ -> h1 __)
   | Bool.False -> (fun _ _ -> h2 __)) __ __

open Div_and_mod

(** val dpi1__o__bool_to_Prop__o__inject :
    (Bool.bool, 'a1) Types.dPair -> __ Types.sig0 **)
let dpi1__o__bool_to_Prop__o__inject x2 =
  __

(** val eject__o__bool_to_Prop__o__inject :
    Bool.bool Types.sig0 -> __ Types.sig0 **)
let eject__o__bool_to_Prop__o__inject x2 =
  __

(** val bool_to_Prop__o__inject : Bool.bool -> __ Types.sig0 **)
let bool_to_Prop__o__inject x1 =
  __

(** val dpi1__o__bool_to_Prop_to_eq__o__inject :
    Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
let dpi1__o__bool_to_Prop_to_eq__o__inject x0 x3 =
  __

(** val eject__o__bool_to_Prop_to_eq__o__inject :
    Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
let eject__o__bool_to_Prop_to_eq__o__inject x0 x3 =
  __

(** val bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
let bool_to_Prop_to_eq__o__inject x0 =
  __

(** val dpi1__o__not_bool_to_Prop_to_eq__o__inject :
    Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
let dpi1__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
  __

(** val eject__o__not_bool_to_Prop_to_eq__o__inject :
    Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
let eject__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
  __

(** val not_bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
let not_bool_to_Prop_to_eq__o__inject x0 =
  __

(** val if_then_else_safe :
    Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let if_then_else_safe b f g =
  (match b with
   | Bool.True -> f
   | Bool.False -> g) __

(** val dpi1__o__not_neq_None__o__inject :
    'a1 Types.option -> (__, 'a2) Types.dPair -> __ Types.sig0 **)
let dpi1__o__not_neq_None__o__inject x1 x4 =
  __

(** val eject__o__not_neq_None__o__inject :
    'a1 Types.option -> __ Types.sig0 -> __ Types.sig0 **)
let eject__o__not_neq_None__o__inject x1 x4 =
  __

(** val not_neq_None__o__inject : 'a1 Types.option -> __ Types.sig0 **)
let not_neq_None__o__inject x1 =
  __

(** val prod_jmdiscr :
    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
let prod_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { Types.fst = a0; Types.snd = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let eq_rect_Type1_r a h x =
  (fun _ auto -> auto) __ h

(** val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **)
let some_Some_elim x y h =
  h __

(** val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2 **)
let pose a auto =
  auto a __

(** val eq_sum :
    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
    Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool **)
let eq_sum leq req left right =
  match left with
  | Types.Inl l ->
    (match right with
     | Types.Inl l' -> leq l l'
     | Types.Inr x -> Bool.False)
  | Types.Inr r ->
    (match right with
     | Types.Inl x -> Bool.False
     | Types.Inr r' -> req r r')

(** val eq_prod :
    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
    Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool **)
let eq_prod leq req left right =
  let { Types.fst = l; Types.snd = r } = left in
  let { Types.fst = l'; Types.snd = r' } = right in
  Bool.andb (leq l l') (req r r')