Function axiom_bitvec_index_req 

pub broadcast proof fn axiom_bitvec_index_req<T: BitStore, O: BitOrder>(
    bv: &BitVec<T, O>,
    i: usize,
)

requires

obeys_bitvec_model::<T, O>(),

ensures

<BitVec<T, O> as IndexSpec<usize>>::index_req(bv, &i) == (i < bitvec_view(bv).len()),

BitVec’s Index precondition (index_req): the index must be in [0, len), the condition under which BitVec::index does not panic.