val rest (#a:Type0) (#len:flen{len > 1}) (s:ntuple a len) : ntuple a (len - 1)
let rest #a #len s =
  normalize_term (rest_ #a #len s)
val rest (#a:Type0) (#len:flen{len > 1}) (s:ntuple a len) : ntuple a (len - 1)
let rest #a #len s =
normalize_term (rest_ #a #len s)
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 Prims.b2t Prims.op_GreaterThan Lib.NTuple.ntuple FStar.Pervasives.normalize_term Prims.op_Subtraction Lib.NTuple.rest_
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))
val rest (#a:Type0) (#len:flen{len > 1}) (s:ntuple a len) : ntuple a (len - 1)
s: Lib.NTuple.ntuple a len -> Lib.NTuple.ntuple a (len - 1)