Function axiom_range_bitslice_get_model 

pub broadcast proof fn axiom_range_bitslice_get_model<'a, T: BitStore, O: BitOrder>()

requires

obeys_bitvec_model::<T, O>(),

ensures

#[trigger] obeys_bitslice_get_model::<'a, T, O, Range<usize>>(),