Function obeys_bitslice_index_model 

pub uninterp spec fn obeys_bitslice_index_model<T: BitStore, O: BitOrder, Idx>() -> bool
where
    BitSlice<T, O>: Index<Idx>,

The only index and get specializations covered by this bridge.