Function obeys_bitslice_get_model 

pub uninterp spec fn obeys_bitslice_get_model<'a, T: BitStore, O: BitOrder, I>() -> bool
where
    I: BitSliceIndex<'a, T, O>,