open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

type 'a list =
| Nil
| Cons of 'a * 'a list

(** val list_rect_Type4 :
    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
let rec list_rect_Type4 h_nil h_cons = function
| Nil -> h_nil
| Cons (x_723, x_722) ->
  h_cons x_723 x_722 (list_rect_Type4 h_nil h_cons x_722)

(** val list_rect_Type3 :
    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
let rec list_rect_Type3 h_nil h_cons = function
| Nil -> h_nil
| Cons (x_733, x_732) ->
  h_cons x_733 x_732 (list_rect_Type3 h_nil h_cons x_732)

(** val list_rect_Type2 :
    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
let rec list_rect_Type2 h_nil h_cons = function
| Nil -> h_nil
| Cons (x_738, x_737) ->
  h_cons x_738 x_737 (list_rect_Type2 h_nil h_cons x_737)

(** val list_rect_Type1 :
    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
let rec list_rect_Type1 h_nil h_cons = function
| Nil -> h_nil
| Cons (x_743, x_742) ->
  h_cons x_743 x_742 (list_rect_Type1 h_nil h_cons x_742)

(** val list_rect_Type0 :
    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
let rec list_rect_Type0 h_nil h_cons = function
| Nil -> h_nil
| Cons (x_748, x_747) ->
  h_cons x_748 x_747 (list_rect_Type0 h_nil h_cons x_747)

(** val list_inv_rect_Type4 :
    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
    -> 'a2 **)
let list_inv_rect_Type4 hterm h1 h2 =
  let hcut = list_rect_Type4 h1 h2 hterm in hcut __

(** val list_inv_rect_Type3 :
    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
    -> 'a2 **)
let list_inv_rect_Type3 hterm h1 h2 =
  let hcut = list_rect_Type3 h1 h2 hterm in hcut __

(** val list_inv_rect_Type2 :
    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
    -> 'a2 **)
let list_inv_rect_Type2 hterm h1 h2 =
  let hcut = list_rect_Type2 h1 h2 hterm in hcut __

(** val list_inv_rect_Type1 :
    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
    -> 'a2 **)
let list_inv_rect_Type1 hterm h1 h2 =
  let hcut = list_rect_Type1 h1 h2 hterm in hcut __

(** val list_inv_rect_Type0 :
    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
    -> 'a2 **)
let list_inv_rect_Type0 hterm h1 h2 =
  let hcut = list_rect_Type0 h1 h2 hterm in hcut __

(** val list_discr : 'a1 list -> 'a1 list -> __ **)
let list_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Nil -> Obj.magic (fun _ dH -> dH)
     | Cons (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val append : 'a1 list -> 'a1 list -> 'a1 list **)
let rec append l1 l2 =
  match l1 with
  | Nil -> l2
  | Cons (hd, tl) -> Cons (hd, (append tl l2))

(** val hd : 'a1 list -> 'a1 -> 'a1 **)
let hd l d =
  match l with
  | Nil -> d
  | Cons (a, x) -> a

(** val tail : 'a1 list -> 'a1 list **)
let tail = function
| Nil -> Nil
| Cons (hd0, tl) -> tl

(** val option_hd : 'a1 list -> 'a1 Types.option **)
let option_hd = function
| Nil -> Types.None
| Cons (a, x) -> Types.Some a

(** val option_cons : 'a1 Types.option -> 'a1 list -> 'a1 list **)
let option_cons c l =
  match c with
  | Types.None -> l
  | Types.Some c0 -> Cons (c0, l)

(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
let rec map f = function
| Nil -> Nil
| Cons (x, tl) -> Cons ((f x), (map f tl))

(** val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2 **)
let rec foldr f b = function
| Nil -> b
| Cons (a, l0) -> f a (foldr f b l0)

(** val filter : ('a1 -> Bool.bool) -> 'a1 list -> 'a1 list **)
let filter p =
  foldr (fun x l0 ->
    match p x with
    | Bool.True -> Cons (x, l0)
    | Bool.False -> l0) Nil

(** val compose : ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list **)
let compose f l1 l2 =
  foldr (fun i acc -> append (map (f i) l2) acc) Nil l1

(** val rev_append : 'a1 list -> 'a1 list -> 'a1 list **)
let rec rev_append l1 l2 =
  match l1 with
  | Nil -> l2
  | Cons (a, tl) -> rev_append tl (Cons (a, l2))

(** val reverse : 'a1 list -> 'a1 list **)
let reverse l =
  rev_append l Nil

(** val length : 'a1 list -> Nat.nat **)
let rec length = function
| Nil -> Nat.O
| Cons (a, tl) -> Nat.S (length tl)

(** val split_rev :
    'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
let rec split_rev l acc = function
| Nat.O -> { Types.fst = acc; Types.snd = l }
| Nat.S m ->
  (match l with
   | Nil -> { Types.fst = acc; Types.snd = Nil }
   | Cons (a, tl) -> split_rev tl (Cons (a, acc)) m)

(** val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
let split l n =
  let { Types.fst = l1; Types.snd = l2 } = split_rev l Nil n in
  { Types.fst = (reverse l1); Types.snd = l2 }

(** val flatten : 'a1 list list -> 'a1 list **)
let flatten l =
  foldr append Nil l

(** val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1 **)
let rec nth n l d =
  match n with
  | Nat.O -> hd l d
  | Nat.S m -> nth m (tail l) d

(** val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option **)
let rec nth_opt n = function
| Nil -> Types.None
| Cons (h, t) ->
  (match n with
   | Nat.O -> Types.Some h
   | Nat.S m -> nth_opt m t)

(** val fold :
    ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
    list -> 'a2 **)
let rec fold op b p f = function
| Nil -> b
| Cons (a, l0) ->
  (match p a with
   | Bool.True -> op (f a) (fold op b p f l0)
   | Bool.False -> fold op b p f l0)

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 **)
let rec aop_rect_Type4 nil h_mk_Aop x_783 =
  let op = x_783 in h_mk_Aop op __ __ __

(** val aop_rect_Type5 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type5 nil h_mk_Aop x_785 =
  let op = x_785 in h_mk_Aop op __ __ __

(** val aop_rect_Type3 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type3 nil h_mk_Aop x_787 =
  let op = x_787 in h_mk_Aop op __ __ __

(** val aop_rect_Type2 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type2 nil h_mk_Aop x_789 =
  let op = x_789 in h_mk_Aop op __ __ __

(** val aop_rect_Type1 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type1 nil h_mk_Aop x_791 =
  let op = x_791 in h_mk_Aop op __ __ __

(** val aop_rect_Type0 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type0 nil h_mk_Aop x_793 =
  let op = x_793 in h_mk_Aop op __ __ __

(** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **)
let rec op nil xxx =
  let yyy = xxx in yyy

(** val aop_inv_rect_Type4 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type4 x2 hterm h1 =
  let hcut = aop_rect_Type4 x2 h1 hterm in hcut __

(** val aop_inv_rect_Type3 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type3 x2 hterm h1 =
  let hcut = aop_rect_Type3 x2 h1 hterm in hcut __

(** val aop_inv_rect_Type2 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type2 x2 hterm h1 =
  let hcut = aop_rect_Type2 x2 h1 hterm in hcut __

(** val aop_inv_rect_Type1 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type1 x2 hterm h1 =
  let hcut = aop_rect_Type1 x2 h1 hterm in hcut __

(** val aop_inv_rect_Type0 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type0 x2 hterm h1 =
  let hcut = aop_rect_Type0 x2 h1 hterm in hcut __

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

(** val dpi1__o__op :
    'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
let dpi1__o__op x1 x3 =
  op x1 x3.Types.dpi1

(** val lhd : 'a1 list -> Nat.nat -> 'a1 list **)
let rec lhd l = function
| Nat.O -> Nil
| Nat.S n0 ->
  (match l with
   | Nil -> Nil
   | Cons (a, l0) -> Cons (a, (lhd l0 n0)))

(** val ltl : 'a1 list -> Nat.nat -> 'a1 list **)
let rec ltl l = function
| Nat.O -> l
| Nat.S n0 -> ltl (tail l) n0

(** val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option **)
let rec find f = function
| Nil -> Types.None
| Cons (h, t) ->
  (match f h with
   | Types.None -> find f t
   | Types.Some b -> Types.Some b)

(** val position_of_aux :
    ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option **)
let rec position_of_aux found l acc =
  match l with
  | Nil -> Types.None
  | Cons (h, t) ->
    (match found h with
     | Bool.True -> Types.Some acc
     | Bool.False -> position_of_aux found t (Nat.S acc))

(** val position_of :
    ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option **)
let position_of found l =
  position_of_aux found l Nat.O

(** val make_list : 'a1 -> Nat.nat -> 'a1 list **)
let rec make_list a = function
| Nat.O -> Nil
| Nat.S m -> Cons (a, (make_list a m))