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