pub broadcast proof fn axiom_fmt_req_all_display<A: Display>(a: &A, f: &Formatter<'_>)
fmt_req_all::<A>(),
#[trigger] a.fmt_req(f),