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 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))
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
Lib.NTuple.flen Lib.NTuple.ntuple Prims.nat Prims.b2t Prims.op_LessThan Prims.op_Equality Prims.int Lib.NTuple.fst Prims.bool Lib.NTuple.index_ Prims.op_Subtraction Lib.NTuple.rest Prims.unit Prims._assert Prims.op_GreaterThan
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
val index_ : s: Lib.NTuple.ntuple a len -> i: Prims.nat{i < len} -> a
s: Lib.NTuple.ntuple a len -> i: Prims.nat{i < len} -> a