open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

type void = unit (* empty inductive *)

(** val void_rect_Type4 : void -> 'a1 **)
let rec void_rect_Type4 x_327 =
  assert false (* absurd case *)

(** val void_rect_Type5 : void -> 'a1 **)
let rec void_rect_Type5 x_328 =
  assert false (* absurd case *)

(** val void_rect_Type3 : void -> 'a1 **)
let rec void_rect_Type3 x_329 =
  assert false (* absurd case *)

(** val void_rect_Type2 : void -> 'a1 **)
let rec void_rect_Type2 x_330 =
  assert false (* absurd case *)

(** val void_rect_Type1 : void -> 'a1 **)
let rec void_rect_Type1 x_331 =
  assert false (* absurd case *)

(** val void_rect_Type0 : void -> 'a1 **)
let rec void_rect_Type0 x_332 =
  assert false (* absurd case *)

type unit0 =
| It

(** val unit_rect_Type4 : 'a1 -> unit0 -> 'a1 **)
let rec unit_rect_Type4 h_it = function
| It -> h_it

(** val unit_rect_Type5 : 'a1 -> unit0 -> 'a1 **)
let rec unit_rect_Type5 h_it = function
| It -> h_it

(** val unit_rect_Type3 : 'a1 -> unit0 -> 'a1 **)
let rec unit_rect_Type3 h_it = function
| It -> h_it

(** val unit_rect_Type2 : 'a1 -> unit0 -> 'a1 **)
let rec unit_rect_Type2 h_it = function
| It -> h_it

(** val unit_rect_Type1 : 'a1 -> unit0 -> 'a1 **)
let rec unit_rect_Type1 h_it = function
| It -> h_it

(** val unit_rect_Type0 : 'a1 -> unit0 -> 'a1 **)
let rec unit_rect_Type0 h_it = function
| It -> h_it

(** val unit_inv_rect_Type4 : unit0 -> (__ -> 'a1) -> 'a1 **)
let unit_inv_rect_Type4 hterm h1 =
  let hcut = unit_rect_Type4 h1 hterm in hcut __

(** val unit_inv_rect_Type3 : unit0 -> (__ -> 'a1) -> 'a1 **)
let unit_inv_rect_Type3 hterm h1 =
  let hcut = unit_rect_Type3 h1 hterm in hcut __

(** val unit_inv_rect_Type2 : unit0 -> (__ -> 'a1) -> 'a1 **)
let unit_inv_rect_Type2 hterm h1 =
  let hcut = unit_rect_Type2 h1 hterm in hcut __

(** val unit_inv_rect_Type1 : unit0 -> (__ -> 'a1) -> 'a1 **)
let unit_inv_rect_Type1 hterm h1 =
  let hcut = unit_rect_Type1 h1 hterm in hcut __

(** val unit_inv_rect_Type0 : unit0 -> (__ -> 'a1) -> 'a1 **)
let unit_inv_rect_Type0 hterm h1 =
  let hcut = unit_rect_Type0 h1 hterm in hcut __

(** val unit_discr : unit0 -> unit0 -> __ **)
let unit_discr x y =
  Logic.eq_rect_Type2 x (let It = x in Obj.magic (fun _ dH -> dH)) y

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

(** val sum_rect_Type4 :
    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
let rec sum_rect_Type4 h_inl h_inr = function
| Inl x_371 -> h_inl x_371
| Inr x_372 -> h_inr x_372

(** val sum_rect_Type5 :
    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
let rec sum_rect_Type5 h_inl h_inr = function
| Inl x_376 -> h_inl x_376
| Inr x_377 -> h_inr x_377

(** val sum_rect_Type3 :
    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
let rec sum_rect_Type3 h_inl h_inr = function
| Inl x_381 -> h_inl x_381
| Inr x_382 -> h_inr x_382

(** val sum_rect_Type2 :
    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
let rec sum_rect_Type2 h_inl h_inr = function
| Inl x_386 -> h_inl x_386
| Inr x_387 -> h_inr x_387

(** val sum_rect_Type1 :
    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
let rec sum_rect_Type1 h_inl h_inr = function
| Inl x_391 -> h_inl x_391
| Inr x_392 -> h_inr x_392

(** val sum_rect_Type0 :
    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
let rec sum_rect_Type0 h_inl h_inr = function
| Inl x_396 -> h_inl x_396
| Inr x_397 -> h_inr x_397

(** val sum_inv_rect_Type4 :
    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
let sum_inv_rect_Type4 hterm h1 h2 =
  let hcut = sum_rect_Type4 h1 h2 hterm in hcut __

(** val sum_inv_rect_Type3 :
    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
let sum_inv_rect_Type3 hterm h1 h2 =
  let hcut = sum_rect_Type3 h1 h2 hterm in hcut __

(** val sum_inv_rect_Type2 :
    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
let sum_inv_rect_Type2 hterm h1 h2 =
  let hcut = sum_rect_Type2 h1 h2 hterm in hcut __

(** val sum_inv_rect_Type1 :
    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
let sum_inv_rect_Type1 hterm h1 h2 =
  let hcut = sum_rect_Type1 h1 h2 hterm in hcut __

(** val sum_inv_rect_Type0 :
    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
let sum_inv_rect_Type0 hterm h1 h2 =
  let hcut = sum_rect_Type0 h1 h2 hterm in hcut __

(** val sum_discr : ('a1, 'a2) sum -> ('a1, 'a2) sum -> __ **)
let sum_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Inl a0 -> Obj.magic (fun _ dH -> dH __)
     | Inr a0 -> Obj.magic (fun _ dH -> dH __)) y

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

(** val option_rect_Type4 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
let rec option_rect_Type4 h_None h_Some = function
| None -> h_None
| Some x_435 -> h_Some x_435

(** val option_rect_Type5 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
let rec option_rect_Type5 h_None h_Some = function
| None -> h_None
| Some x_439 -> h_Some x_439

(** val option_rect_Type3 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
let rec option_rect_Type3 h_None h_Some = function
| None -> h_None
| Some x_443 -> h_Some x_443

(** val option_rect_Type2 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
let rec option_rect_Type2 h_None h_Some = function
| None -> h_None
| Some x_447 -> h_Some x_447

(** val option_rect_Type1 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
let rec option_rect_Type1 h_None h_Some = function
| None -> h_None
| Some x_451 -> h_Some x_451

(** val option_rect_Type0 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
let rec option_rect_Type0 h_None h_Some = function
| None -> h_None
| Some x_455 -> h_Some x_455

(** val option_inv_rect_Type4 :
    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
let option_inv_rect_Type4 hterm h1 h2 =
  let hcut = option_rect_Type4 h1 h2 hterm in hcut __

(** val option_inv_rect_Type3 :
    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
let option_inv_rect_Type3 hterm h1 h2 =
  let hcut = option_rect_Type3 h1 h2 hterm in hcut __

(** val option_inv_rect_Type2 :
    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
let option_inv_rect_Type2 hterm h1 h2 =
  let hcut = option_rect_Type2 h1 h2 hterm in hcut __

(** val option_inv_rect_Type1 :
    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
let option_inv_rect_Type1 hterm h1 h2 =
  let hcut = option_rect_Type1 h1 h2 hterm in hcut __

(** val option_inv_rect_Type0 :
    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
let option_inv_rect_Type0 hterm h1 h2 =
  let hcut = option_rect_Type0 h1 h2 hterm in hcut __

(** val option_discr : 'a1 option -> 'a1 option -> __ **)
let option_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | None -> Obj.magic (fun _ dH -> dH)
     | Some a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val option_map : ('a1 -> 'a2) -> 'a1 option -> 'a2 option **)
let option_map f = function
| None -> None
| Some a -> Some (f a)

(** val option_map_def : ('a1 -> 'a2) -> 'a2 -> 'a1 option -> 'a2 **)
let option_map_def f d = function
| None -> d
| Some a -> f a

(** val refute_none_by_refl :
    ('a1 -> 'a2) -> 'a1 option -> ('a1 -> __ -> 'a3) -> 'a3 **)
let refute_none_by_refl p clearme x =
  (match clearme with
   | None -> (fun _ -> assert false (* absurd case *))
   | Some a -> (fun _ p0 -> p0 a __)) __ x

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

(** val dPair_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
let rec dPair_rect_Type4 h_mk_DPair x_484 =
  let { dpi1 = dpi3; dpi2 = dpi4 } = x_484 in h_mk_DPair dpi3 dpi4

(** val dPair_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
let rec dPair_rect_Type5 h_mk_DPair x_486 =
  let { dpi1 = dpi3; dpi2 = dpi4 } = x_486 in h_mk_DPair dpi3 dpi4

(** val dPair_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
let rec dPair_rect_Type3 h_mk_DPair x_488 =
  let { dpi1 = dpi3; dpi2 = dpi4 } = x_488 in h_mk_DPair dpi3 dpi4

(** val dPair_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
let rec dPair_rect_Type2 h_mk_DPair x_490 =
  let { dpi1 = dpi3; dpi2 = dpi4 } = x_490 in h_mk_DPair dpi3 dpi4

(** val dPair_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
let rec dPair_rect_Type1 h_mk_DPair x_492 =
  let { dpi1 = dpi3; dpi2 = dpi4 } = x_492 in h_mk_DPair dpi3 dpi4

(** val dPair_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
let rec dPair_rect_Type0 h_mk_DPair x_494 =
  let { dpi1 = dpi3; dpi2 = dpi4 } = x_494 in h_mk_DPair dpi3 dpi4

(** val dpi1 : ('a1, 'a2) dPair -> 'a1 **)
let rec dpi1 xxx =
  xxx.dpi1

(** val dpi2 : ('a1, 'a2) dPair -> 'a2 **)
let rec dpi2 xxx =
  xxx.dpi2

(** val dPair_inv_rect_Type4 :
    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let dPair_inv_rect_Type4 hterm h1 =
  let hcut = dPair_rect_Type4 h1 hterm in hcut __

(** val dPair_inv_rect_Type3 :
    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let dPair_inv_rect_Type3 hterm h1 =
  let hcut = dPair_rect_Type3 h1 hterm in hcut __

(** val dPair_inv_rect_Type2 :
    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let dPair_inv_rect_Type2 hterm h1 =
  let hcut = dPair_rect_Type2 h1 hterm in hcut __

(** val dPair_inv_rect_Type1 :
    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let dPair_inv_rect_Type1 hterm h1 =
  let hcut = dPair_rect_Type1 h1 hterm in hcut __

(** val dPair_inv_rect_Type0 :
    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let dPair_inv_rect_Type0 hterm h1 =
  let hcut = dPair_rect_Type0 h1 hterm in hcut __

(** val dPair_discr : ('a1, 'a2) dPair -> ('a1, 'a2) dPair -> __ **)
let dPair_discr x y =
  Logic.eq_rect_Type2 x
    (let { dpi1 = a0; dpi2 = a10 } = x in Obj.magic (fun _ dH -> dH __ __)) y

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

(** val sig_rect_Type4 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
let rec sig_rect_Type4 h_mk_Sig x_510 =
  let pi1 = x_510 in h_mk_Sig pi1 __

(** val sig_rect_Type5 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
let rec sig_rect_Type5 h_mk_Sig x_512 =
  let pi1 = x_512 in h_mk_Sig pi1 __

(** val sig_rect_Type3 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
let rec sig_rect_Type3 h_mk_Sig x_514 =
  let pi1 = x_514 in h_mk_Sig pi1 __

(** val sig_rect_Type2 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
let rec sig_rect_Type2 h_mk_Sig x_516 =
  let pi1 = x_516 in h_mk_Sig pi1 __

(** val sig_rect_Type1 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
let rec sig_rect_Type1 h_mk_Sig x_518 =
  let pi1 = x_518 in h_mk_Sig pi1 __

(** val sig_rect_Type0 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
let rec sig_rect_Type0 h_mk_Sig x_520 =
  let pi1 = x_520 in h_mk_Sig pi1 __

(** val pi1 : 'a1 sig0 -> 'a1 **)
let rec pi1 xxx =
  let yyy = xxx in yyy

(** val sig_inv_rect_Type4 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
let sig_inv_rect_Type4 hterm h1 =
  let hcut = sig_rect_Type4 h1 hterm in hcut __

(** val sig_inv_rect_Type3 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
let sig_inv_rect_Type3 hterm h1 =
  let hcut = sig_rect_Type3 h1 hterm in hcut __

(** val sig_inv_rect_Type2 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
let sig_inv_rect_Type2 hterm h1 =
  let hcut = sig_rect_Type2 h1 hterm in hcut __

(** val sig_inv_rect_Type1 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
let sig_inv_rect_Type1 hterm h1 =
  let hcut = sig_rect_Type1 h1 hterm in hcut __

(** val sig_inv_rect_Type0 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
let sig_inv_rect_Type0 hterm h1 =
  let hcut = sig_rect_Type0 h1 hterm in hcut __

(** val sig_discr : 'a1 sig0 -> 'a1 sig0 -> __ **)
let sig_discr x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y

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

(** val prod_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
let rec prod_rect_Type4 h_mk_Prod x_536 =
  let { fst = fst0; snd = snd0 } = x_536 in h_mk_Prod fst0 snd0

(** val prod_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
let rec prod_rect_Type5 h_mk_Prod x_538 =
  let { fst = fst0; snd = snd0 } = x_538 in h_mk_Prod fst0 snd0

(** val prod_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
let rec prod_rect_Type3 h_mk_Prod x_540 =
  let { fst = fst0; snd = snd0 } = x_540 in h_mk_Prod fst0 snd0

(** val prod_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
let rec prod_rect_Type2 h_mk_Prod x_542 =
  let { fst = fst0; snd = snd0 } = x_542 in h_mk_Prod fst0 snd0

(** val prod_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
let rec prod_rect_Type1 h_mk_Prod x_544 =
  let { fst = fst0; snd = snd0 } = x_544 in h_mk_Prod fst0 snd0

(** val prod_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
let rec prod_rect_Type0 h_mk_Prod x_546 =
  let { fst = fst0; snd = snd0 } = x_546 in h_mk_Prod fst0 snd0

(** val fst : ('a1, 'a2) prod -> 'a1 **)
let rec fst xxx =
  xxx.fst

(** val snd : ('a1, 'a2) prod -> 'a2 **)
let rec snd xxx =
  xxx.snd

(** val prod_inv_rect_Type4 :
    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let prod_inv_rect_Type4 hterm h1 =
  let hcut = prod_rect_Type4 h1 hterm in hcut __

(** val prod_inv_rect_Type3 :
    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let prod_inv_rect_Type3 hterm h1 =
  let hcut = prod_rect_Type3 h1 hterm in hcut __

(** val prod_inv_rect_Type2 :
    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let prod_inv_rect_Type2 hterm h1 =
  let hcut = prod_rect_Type2 h1 hterm in hcut __

(** val prod_inv_rect_Type1 :
    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let prod_inv_rect_Type1 hterm h1 =
  let hcut = prod_rect_Type1 h1 hterm in hcut __

(** val prod_inv_rect_Type0 :
    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
let prod_inv_rect_Type0 hterm h1 =
  let hcut = prod_rect_Type0 h1 hterm in hcut __

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

(** val coerc_pair_sigma : ('a1, 'a2) prod -> ('a1, 'a2 sig0) prod **)
let coerc_pair_sigma clearme =
  (let { fst = a; snd = b } = clearme in (fun _ -> { fst = a; snd = b })) __

(** val dpi1__o__coerc_pair_sigma :
    (('a1, 'a2) prod, 'a3) dPair -> ('a1, 'a2 sig0) prod **)
let dpi1__o__coerc_pair_sigma x4 =
  coerc_pair_sigma x4.dpi1