Function axiom_fmt_req_all_upper_hex 

pub broadcast proof fn axiom_fmt_req_all_upper_hex<A: UpperHex>(a: &A, f: &Formatter<'_>)

requires

fmt_req_all::<A>(),

ensures

#[trigger] a.fmt_req(f),