pub broadcast proof fn to_string_from_display_ensures_for_str(t: &str, res: String)Expand description
ensures
#[trigger] to_string_from_display_ensures::<str>(t, res) <==> (t@ == res@),