Function axiom_bitslice_get_range 

pub broadcast proof fn axiom_bitslice_get_range<'a, T: BitStore, O: BitOrder>(
    bv: &BitSlice<T, O>,
    range: Range<usize>,
)

requires

obeys_bitvec_model::<T, O>(),

ensures

match bitslice_get_value(bv, range) {
    Some(s) => (
        &&& 0 <= range.start <= range.end <= bitslice_view(bv).len()
        &&& bitslice_view(s) == bitslice_view(bv)[range.start..range.end]

    ),
    None => !(0 <= range.start <= range.end <= bitslice_view(bv).len()),
},

For a Range<usize>, get returns Some of a bit-slice equal to the sub-range bitslice_view(bv)[start..end] when 0 <= start <= end <= bitslice_view(bv).len(), and None otherwise.