val createi_lemma_
      (#a: Type0)
      (min: nat)
      (max: flen{max > min})
      (f: (i: nat{i < max} -> a))
      (i: nat{i < max - min})
    : Lemma (ensures (index #a #(max - min) (createi_ #a min max f) i == f (min + i))) (decreases i)
let rec createi_lemma_ (#a:Type0) (min:nat) (max:flen{max > min}) (f:(i:nat{i < max} -> a)) (i:nat{i < max - min}) :
  Lemma (ensures (index #a #(max - min) (createi_ #a min max f) i == f (min+i))) (decreases i)
 =
  if i = 0 then ()
  else createi_lemma_ #a (min+1) max f (i-1)
val createi_lemma_
      (#a: Type0)
      (min: nat)
      (max: flen{max > min})
      (f: (i: nat{i < max} -> a))
      (i: nat{i < max - min})
    : Lemma (ensures (index #a #(max - min) (createi_ #a min max f) i == f (min + i))) (decreases i)
let rec createi_lemma_
      (#a: Type0)
      (min: nat)
      (max: flen{max > min})
      (f: (i: nat{i < max} -> a))
      (i: nat{i < max - min})
    : Lemma (ensures (index #a #(max - min) (createi_ #a min max f) i == f (min + i))) (decreases i) =
if i = 0 then () else createi_lemma_ #a (min + 1) max f (i - 1)
Lib.NTuple.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Lib.NTuple.fst
Prims.nat Lib.NTuple.flen Prims.b2t Prims.op_GreaterThan Prims.op_LessThan Prims.op_Subtraction Prims.op_Equality Prims.int Prims.bool Lib.NTuple.createi_lemma_ Prims.op_Addition Prims.unit Prims.l_True Prims.squash Prims.eq2 Lib.NTuple.index Lib.NTuple.createi_ Prims.Nil FStar.Pervasives.pattern
module Lib.NTuple

open FStar.Mul
open Lib.IntTypes

#set-options "--z3rlimit 15 --ifuel 0 --fuel 1"

let max_ntuple_len = max_size_t

unfold let length (#a:Type0) (#len:flen) (s: ntuple a len) : flen = len

inline_for_extraction
let fst_ (#a:Type0) (#len:flen) (s:ntuple_ a len) : a =
  if len = 1 then s
  else fst (s <: a & ntuple_ a (len - 1))

let fst #a #len (s:ntuple a len) =
  normalize_term (fst_ #a #len s)

inline_for_extraction
let rest_ (#a:Type0) (#len:flen{len > 1}) (s:ntuple_ a len) : ntuple_ a (len - 1)=
    snd (s <: a & ntuple_ a (len - 1))

let rest #a #len s =
  normalize_term (rest_ #a #len s)

inline_for_extraction
let rec index_ (#a:Type0) (#len:flen) (s:ntuple a len) (i:nat{i < len}) =
  if i = 0 then fst s
  else (assert (len > 1);
        index_ #a #(len-1) (rest s) (i-1))

let index #a #len s i =
  normalize_term (index_ s i)

let index_fst_lemma #a #len s = ()

inline_for_extraction
let rec createi_ (#a:Type0) (min:nat) (max:flen{max > min}) (f:(i:nat{i < max} -> a)) :
  Tot (ntuple_ a (max - min)) (decreases (max - min))
 =
  if min + 1 = max then f min
  else f min, createi_ #a (min+1) max f

let createi #a len f =
  normalize_term (createi_ #a 0 len f)

inline_for_extraction
let rec gcreatei_ (#a:Type0) (min:nat) (max:flen{max > min}) (f:(i:nat{i < max} -> GTot a)) :
  GTot (ntuple_ a (max - min)) (decreases (max - min))
 =
  if min + 1 = max then f min
  else f min, gcreatei_ #a (min+1) max f

let gcreatei #a len f =
  normalize_term (gcreatei_ #a 0 len f)

let rec createi_lemma_ (#a:Type0) (min:nat) (max:flen{max > min}) (f:(i:nat{i < max} -> a)) (i:nat{i < max - min}) :
  Lemma (ensures (index #a #(max - min) (createi_ #a min max f) i == f (min+i))) (decreases i)
val createi_lemma_
      (#a: Type0)
      (min: nat)
      (max: flen{max > min})
      (f: (i: nat{i < max} -> a))
      (i: nat{i < max - min})
    : Lemma (ensures (index #a #(max - min) (createi_ #a min max f) i == f (min + i))) (decreases i)

    min: Prims.nat ->
    max: Lib.NTuple.flen{max > min} ->
    f: (i: Prims.nat{i < max} -> a) ->
    i: Prims.nat{i < max - min}
  -> FStar.Pervasives.Lemma
      (ensures Lib.NTuple.index (Lib.NTuple.createi_ min max f) i == f (min + i)) (decreases i)