Function obeys_bitvec_model 

pub uninterp spec fn obeys_bitvec_model<T: BitStore, O: BitOrder>() -> bool

Whether storage and order support the immutable sequence model. Only the concrete instances in group_bitvec_models are trusted below.