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