val fst_ (#a: Type0) (#len: flen) (s: ntuple_ a len) : a
let fst_ (#a:Type0) (#len:flen) (s:ntuple_ a len) : a =
  if len = 1 then s
  else fst (s <: a & ntuple_ a (len - 1))
val fst_ (#a: Type0) (#len: flen) (s: ntuple_ a len) : a
let fst_ (#a: Type0) (#len: flen) (s: ntuple_ a len) : a =
if len = 1 then s else fst (s <: a & ntuple_ a (len - 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.op_Equality Prims.int Prims.bool FStar.Pervasives.Native.fst Prims.op_Subtraction FStar.Pervasives.Native.tuple2
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
val fst_ (#a: Type0) (#len: flen) (s: ntuple_ a len) : a
s: Lib.NTuple.ntuple_ a len -> a