pub proof fn lemma_base128_fmt_sound_nonmal_inv()Expand description
ensures
base128_fmt::<true>().sound_inv(),base128_fmt::<true>().nonmal_inv(),pub proof fn lemma_base128_fmt_sound_nonmal_inv()base128_fmt::<true>().sound_inv(),base128_fmt::<true>().nonmal_inv(),