val array_index : s: FStar.ImmutableArray.Base.t _ -> i: Prims.nat{i < FStar.ImmutableArray.Base.length s} -> _
let array_index = FStar.ImmutableArray.index
module Util.ImmutableArray

open FStar.ImmutableArray
open Spec.List
open Spec.Ubool
open Util.List
open Util.Nth
open Util.Range

let array_t = FStar.ImmutableArray.t
/
Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.ImmutableArray.fsti.checked
Util.ImmutableArray.fsti
s: FStar.ImmutableArray.Base.t _ -> i: Prims.nat{i < FStar.ImmutableArray.Base.length s} -> _
FStar.ImmutableArray.Base.index FStar.ImmutableArray.Base.t Prims.nat Prims.b2t Prims.op_LessThan FStar.ImmutableArray.Base.length
let array_index =
  
FStar.ImmutableArray.index