Function bitslice_get_value 

pub uninterp spec fn bitslice_get_value<'a, T: BitStore, O: BitOrder, I: BitSliceIndex<'a, T, O>>(
    bv: &BitSlice<T, O>,
    idx: I,
) -> Option<<I as BitSliceIndex<'a, T, O>>::Immut>

Borrows a part of the bit-slice (get is generic over I); the Range<usize> result is related to a sub-range by axiom_bitslice_get_range.