pub broadcast proof fn axiom_u8_bitvec_model()Expand description
ensures
#[trigger] obeys_bitvec_model::<u8, Lsb0>(),pub broadcast proof fn axiom_u8_bitvec_model()#[trigger] obeys_bitvec_model::<u8, Lsb0>(),