pub broadcast proof fn char_u32_cast(c: char, u: u32)Expand description
requires
u == #[trigger] (c as u32),#[trigger] (u as char) == c,Ensures that a char, when cast to a u32, can be cast back to a char.