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

val list_rect_Type3 :
  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2

val list_rect_Type2 :
  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2

val list_rect_Type1 :
  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2

val list_rect_Type0 :
  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2

val list_inv_rect_Type4 :
  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  'a2

val list_inv_rect_Type3 :
  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  'a2

val list_inv_rect_Type2 :
  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  'a2

val list_inv_rect_Type1 :
  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  'a2

val list_inv_rect_Type0 :
  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
  'a2

val list_discr : 'a1 list -> 'a1 list -> __

val append : 'a1 list -> 'a1 list -> 'a1 list

val hd : 'a1 list -> 'a1 -> 'a1

val tail : 'a1 list -> 'a1 list

val option_hd : 'a1 list -> 'a1 Types.option

val option_cons : 'a1 Types.option -> 'a1 list -> 'a1 list

val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list

val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2

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

val compose : ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list

val rev_append : 'a1 list -> 'a1 list -> 'a1 list

val reverse : 'a1 list -> 'a1 list

val length : 'a1 list -> Nat.nat

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

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

val flatten : 'a1 list list -> 'a1 list

val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1

val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option

val fold :
  ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
  list -> 'a2

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

val lhd : 'a1 list -> Nat.nat -> 'a1 list

val ltl : 'a1 list -> Nat.nat -> 'a1 list

val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option

val position_of_aux :
  ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option

val position_of : ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option

val make_list : 'a1 -> Nat.nat -> 'a1 list