Function axiom_bitvec_index_usize 

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

requires

obeys_bitvec_model::<T, O>(),

ensures

*bitvec_index_value(bv, idx) == bitvec_view(bv)[idx as int],

The indexed usize bit equals the model value.