open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Div_and_mod

open Jmeq

open Russell

open Util

open Setoids

open Monad

open Option

open Extranat

type 'a vector =
| VEmpty
| VCons of Nat.nat * 'a * 'a vector

val vector_rect_Type4 :
  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  vector -> 'a2

val vector_rect_Type3 :
  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  vector -> 'a2

val vector_rect_Type2 :
  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  vector -> 'a2

val vector_rect_Type1 :
  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  vector -> 'a2

val vector_rect_Type0 :
  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  vector -> 'a2

val vector_inv_rect_Type4 :
  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2

val vector_inv_rect_Type3 :
  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2

val vector_inv_rect_Type2 :
  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2

val vector_inv_rect_Type1 :
  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2

val vector_inv_rect_Type0 :
  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2

val vector_discr : Nat.nat -> 'a1 vector -> 'a1 vector -> __

val vector_jmdiscr : Nat.nat -> 'a1 vector -> 'a1 vector -> __

val get_index_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1

val get_index' : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1

val get_index_weak_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 Types.option

val set_index : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector

val set_index_weak :
  Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector Types.option

val drop : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 vector Types.option

val head' : Nat.nat -> 'a1 vector -> 'a1

val tail : Nat.nat -> 'a1 vector -> 'a1 vector

val vsplit' :
  Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod

val vsplit :
  Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod

val head : Nat.nat -> 'a1 vector -> ('a1, 'a1 vector) Types.prod

val from_singl : 'a1 vector -> 'a1

val fold_right : Nat.nat -> ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2

val fold_right_i :
  Nat.nat -> (Nat.nat -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2

val fold_right2_i :
  (Nat.nat -> 'a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> Nat.nat -> 'a1 vector ->
  'a2 vector -> 'a3

val fold_left : Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1

val map : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector

val zip_with :
  Nat.nat -> ('a1 -> 'a2 -> 'a3) -> 'a1 vector -> 'a2 vector -> 'a3 vector

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

val replicate : Nat.nat -> 'a1 -> 'a1 vector

val append : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector

val scan_left :
  Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 vector

val scan_right :
  Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a2 -> 'a1 vector -> 'a1 List.list

val revapp : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector

val reverse : Nat.nat -> 'a1 vector -> 'a1 vector

val pad_vector : 'a1 -> Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector

val list_of_vector : Nat.nat -> 'a1 vector -> 'a1 List.list

val vector_of_list : 'a1 List.list -> 'a1 vector

val rotate_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector

val rotate_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector

val shift_left_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector

val switch_bv_plus : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector

val shift_right_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector

val shift_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector

val shift_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector

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

val vector_inv_n : Nat.nat -> 'a1 vector -> __

val eq_v_elim :
  ('a2 -> 'a2 -> Bool.bool) -> (__ -> 'a2 -> 'a2 -> (__ -> __) -> (__ -> __)
  -> __) -> Nat.nat -> 'a2 vector -> 'a2 vector -> (__ -> 'a1) -> (__ -> 'a1)
  -> 'a1

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

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

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

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

val rvsplit : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector vector

val vflatten : Nat.nat -> Nat.nat -> 'a1 vector vector -> 'a1 vector