val index : Type0
let index = nat
module BoolRefinement
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
module L = FStar.List.Tot
open FStar.List.Tot
#push-options "--z3cliopt 'smt.qi.eager_threshold=100' --z3cliopt 'smt.arith.nl=false'"
/
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Stubs.Tactics.V2.Builtins.fsti.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
BoolRefinement.fst
Type0
Prims.nat
let index =
  
nat