open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

type void = unit (* empty inductive *)

val void_rect_Type4 : void -> 'a1

val void_rect_Type5 : void -> 'a1

val void_rect_Type3 : void -> 'a1

val void_rect_Type2 : void -> 'a1

val void_rect_Type1 : void -> 'a1

val void_rect_Type0 : void -> 'a1

type unit0 =
| It

val unit_rect_Type4 : 'a1 -> unit0 -> 'a1

val unit_rect_Type5 : 'a1 -> unit0 -> 'a1

val unit_rect_Type3 : 'a1 -> unit0 -> 'a1

val unit_rect_Type2 : 'a1 -> unit0 -> 'a1

val unit_rect_Type1 : 'a1 -> unit0 -> 'a1

val unit_rect_Type0 : 'a1 -> unit0 -> 'a1

val unit_inv_rect_Type4 : unit0 -> (__ -> 'a1) -> 'a1

val unit_inv_rect_Type3 : unit0 -> (__ -> 'a1) -> 'a1

val unit_inv_rect_Type2 : unit0 -> (__ -> 'a1) -> 'a1

val unit_inv_rect_Type1 : unit0 -> (__ -> 'a1) -> 'a1

val unit_inv_rect_Type0 : unit0 -> (__ -> 'a1) -> 'a1

val unit_discr : unit0 -> unit0 -> __

type ('a, 'b) sum =
| Inl of 'a
| Inr of 'b

val sum_rect_Type4 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3

val sum_rect_Type5 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3

val sum_rect_Type3 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3

val sum_rect_Type2 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3

val sum_rect_Type1 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3

val sum_rect_Type0 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3

val sum_inv_rect_Type4 :
  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3

val sum_inv_rect_Type3 :
  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3

val sum_inv_rect_Type2 :
  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3

val sum_inv_rect_Type1 :
  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3

val sum_inv_rect_Type0 :
  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3

val sum_discr : ('a1, 'a2) sum -> ('a1, 'a2) sum -> __

type 'a option =
| None
| Some of 'a

val option_rect_Type4 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2

val option_rect_Type5 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2

val option_rect_Type3 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2

val option_rect_Type2 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2

val option_rect_Type1 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2

val option_rect_Type0 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2

val option_inv_rect_Type4 :
  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2

val option_inv_rect_Type3 :
  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2

val option_inv_rect_Type2 :
  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2

val option_inv_rect_Type1 :
  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2

val option_inv_rect_Type0 :
  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2

val option_discr : 'a1 option -> 'a1 option -> __

val option_map : ('a1 -> 'a2) -> 'a1 option -> 'a2 option

val option_map_def : ('a1 -> 'a2) -> 'a2 -> 'a1 option -> 'a2

val refute_none_by_refl :
  ('a1 -> 'a2) -> 'a1 option -> ('a1 -> __ -> 'a3) -> 'a3

type ('a, 'f) dPair = { dpi1 : 'a; dpi2 : 'f }

val dPair_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3

val dPair_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3

val dPair_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3

val dPair_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3

val dPair_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3

val dPair_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3

val dpi1 : ('a1, 'a2) dPair -> 'a1

val dpi2 : ('a1, 'a2) dPair -> 'a2

val dPair_inv_rect_Type4 :
  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val dPair_inv_rect_Type3 :
  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val dPair_inv_rect_Type2 :
  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val dPair_inv_rect_Type1 :
  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val dPair_inv_rect_Type0 :
  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val dPair_discr : ('a1, 'a2) dPair -> ('a1, 'a2) dPair -> __

type 'a sig0 =
  'a
  (* singleton inductive, whose constructor was mk_Sig *)

val sig_rect_Type4 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2

val sig_rect_Type5 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2

val sig_rect_Type3 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2

val sig_rect_Type2 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2

val sig_rect_Type1 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2

val sig_rect_Type0 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2

val pi1 : 'a1 sig0 -> 'a1

val sig_inv_rect_Type4 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2

val sig_inv_rect_Type3 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2

val sig_inv_rect_Type2 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2

val sig_inv_rect_Type1 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2

val sig_inv_rect_Type0 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2

val sig_discr : 'a1 sig0 -> 'a1 sig0 -> __

type ('a, 'b) prod = { fst : 'a; snd : 'b }

val prod_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3

val prod_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3

val prod_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3

val prod_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3

val prod_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3

val prod_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3

val fst : ('a1, 'a2) prod -> 'a1

val snd : ('a1, 'a2) prod -> 'a2

val prod_inv_rect_Type4 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val prod_inv_rect_Type3 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val prod_inv_rect_Type2 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val prod_inv_rect_Type1 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val prod_inv_rect_Type0 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val prod_discr : ('a1, 'a2) prod -> ('a1, 'a2) prod -> __

val coerc_pair_sigma : ('a1, 'a2) prod -> ('a1, 'a2 sig0) prod

val dpi1__o__coerc_pair_sigma :
  (('a1, 'a2) prod, 'a3) dPair -> ('a1, 'a2 sig0) prod