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

val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1

val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1

val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1

val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1

val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1

val dAEMONXXX_inv_rect_Type4 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val dAEMONXXX_inv_rect_Type3 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val dAEMONXXX_inv_rect_Type2 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val dAEMONXXX_inv_rect_Type1 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val dAEMONXXX_inv_rect_Type0 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __

val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __

val ltb : Nat.nat -> Nat.nat -> Bool.bool

val geb : Nat.nat -> Nat.nat -> Bool.bool

val gtb : Nat.nat -> Nat.nat -> Bool.bool

val eq_nat : Nat.nat -> Nat.nat -> Bool.bool

val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool

val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list

val fold_left2 :
  ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list -> 'a1

val remove_n_first_internal :
  Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list

val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list

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

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

val foldi_from :
  Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
  List.list -> 'a1 List.list -> 'a1 List.list

val foldi_until :
  Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
  List.list -> 'a1 List.list -> 'a1 List.list

val foldi :
  (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list -> 'a1
  List.list -> 'a1 List.list

val hd_safe : 'a1 List.list -> 'a1

val tail_safe : 'a1 List.list -> 'a1 List.list

val safe_split :
  'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod

val nth_safe : Nat.nat -> 'a1 List.list -> 'a1

val last_safe : 'a1 List.list -> 'a1

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

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

val map2_opt :
  ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
  Types.option

val map2 :
  ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list

val map3 :
  ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
  List.list -> 'a4 List.list

val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2

val safe_nth : Nat.nat -> 'a1 List.list -> 'a1

val nub_by_internal :
  ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list

val nub_by : ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list

val member : ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool

val take : Nat.nat -> 'a1 List.list -> 'a1 List.list

val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list

val list_split :
  Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod

val mapi_internal :
  Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list

val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list

val zip_pottier :
  'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list

val zip_safe :
  'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list

val zip :
  'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
  Types.option

val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1

val rev : 'a1 List.list -> 'a1 List.list

val fold_left_i_aux :
  (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1

val fold_left_i :
  (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1

val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2

val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1

val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat

val division : Nat.nat -> Nat.nat -> Nat.nat

val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat

val modulus : Nat.nat -> Nat.nat -> Nat.nat

val divide_with_remainder :
  Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod

val less_than_or_equal_b_elim :
  Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

open Div_and_mod

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

val eject__o__bool_to_Prop__o__inject : Bool.bool Types.sig0 -> __ Types.sig0

val bool_to_Prop__o__inject : Bool.bool -> __ Types.sig0

val dpi1__o__bool_to_Prop_to_eq__o__inject :
  Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0

val eject__o__bool_to_Prop_to_eq__o__inject :
  Bool.bool -> __ Types.sig0 -> __ Types.sig0

val bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0

val dpi1__o__not_bool_to_Prop_to_eq__o__inject :
  Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0

val eject__o__not_bool_to_Prop_to_eq__o__inject :
  Bool.bool -> __ Types.sig0 -> __ Types.sig0

val not_bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0

val if_then_else_safe : Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val dpi1__o__not_neq_None__o__inject :
  'a1 Types.option -> (__, 'a2) Types.dPair -> __ Types.sig0

val eject__o__not_neq_None__o__inject :
  'a1 Types.option -> __ Types.sig0 -> __ Types.sig0

val not_neq_None__o__inject : 'a1 Types.option -> __ Types.sig0

val prod_jmdiscr : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __

val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2

val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2

val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2

val eq_sum :
  ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
  Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool

val eq_prod :
  ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
  Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool