open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open Div_and_mod

val prodF :
  (Nat.nat -> 'a1) -> (Nat.nat -> 'a2) -> Nat.nat -> Nat.nat -> ('a1, 'a2)
  Types.prod

val bigop :
  Nat.nat -> (Nat.nat -> Bool.bool) -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> (Nat.nat
  -> 'a1) -> 'a1

type 'a aop =
  'a -> 'a -> 'a
  (* singleton inductive, whose constructor was mk_Aop *)

val aop_rect_Type4 :
  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2

val aop_rect_Type5 :
  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2

val aop_rect_Type3 :
  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2

val aop_rect_Type2 :
  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2

val aop_rect_Type1 :
  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2

val aop_rect_Type0 :
  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2

val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1

val aop_inv_rect_Type4 :
  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  'a2

val aop_inv_rect_Type3 :
  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  'a2

val aop_inv_rect_Type2 :
  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  'a2

val aop_inv_rect_Type1 :
  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  'a2

val aop_inv_rect_Type0 :
  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
  'a2

val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __

val dpi1__o__op : 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1

type 'a aCop =
  'a aop
  (* singleton inductive, whose constructor was mk_ACop *)

val aCop_rect_Type4 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2

val aCop_rect_Type5 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2

val aCop_rect_Type3 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2

val aCop_rect_Type2 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2

val aCop_rect_Type1 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2

val aCop_rect_Type0 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2

val aop0 : 'a1 -> 'a1 aCop -> 'a1 aop

val aCop_inv_rect_Type4 :
  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2

val aCop_inv_rect_Type3 :
  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2

val aCop_inv_rect_Type2 :
  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2

val aCop_inv_rect_Type1 :
  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2

val aCop_inv_rect_Type0 :
  'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2

val aCop_discr : 'a1 -> 'a1 aCop -> 'a1 aCop -> __

val dpi1__o__aop__o__op :
  'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1

val aop__o__op : 'a1 -> 'a1 aCop -> 'a1 -> 'a1 -> 'a1

val dpi1__o__aop : 'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 aop

type 'a range = { enum : (Nat.nat -> 'a); upto : Nat.nat;
                  filter : (Nat.nat -> Bool.bool) }

val range_rect_Type4 :
  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
  -> 'a2

val range_rect_Type5 :
  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
  -> 'a2

val range_rect_Type3 :
  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
  -> 'a2

val range_rect_Type2 :
  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
  -> 'a2

val range_rect_Type1 :
  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
  -> 'a2

val range_rect_Type0 :
  ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
  -> 'a2

val enum : 'a1 range -> Nat.nat -> 'a1

val upto : 'a1 range -> Nat.nat

val filter : 'a1 range -> Nat.nat -> Bool.bool

val range_inv_rect_Type4 :
  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
  -> 'a2) -> 'a2

val range_inv_rect_Type3 :
  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
  -> 'a2) -> 'a2

val range_inv_rect_Type2 :
  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
  -> 'a2) -> 'a2

val range_inv_rect_Type1 :
  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
  -> 'a2) -> 'a2

val range_inv_rect_Type0 :
  'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
  -> 'a2) -> 'a2

val range_discr : 'a1 range -> 'a1 range -> __

type 'a dop = { sum0 : 'a aCop; prod0 : ('a -> 'a -> 'a) }

val dop_rect_Type4 :
  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
  'a2

val dop_rect_Type5 :
  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
  'a2

val dop_rect_Type3 :
  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
  'a2

val dop_rect_Type2 :
  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
  'a2

val dop_rect_Type1 :
  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
  'a2

val dop_rect_Type0 :
  'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
  'a2

val sum0 : 'a1 -> 'a1 dop -> 'a1 aCop

val prod0 : 'a1 -> 'a1 dop -> 'a1 -> 'a1 -> 'a1

val dop_inv_rect_Type4 :
  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
  'a2) -> 'a2

val dop_inv_rect_Type3 :
  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
  'a2) -> 'a2

val dop_inv_rect_Type2 :
  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
  'a2) -> 'a2

val dop_inv_rect_Type1 :
  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
  'a2) -> 'a2

val dop_inv_rect_Type0 :
  'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
  'a2) -> 'a2

val dop_discr : 'a1 -> 'a1 dop -> 'a1 dop -> __