Function axiom_fmt_req_all_ref 

pub broadcast proof fn axiom_fmt_req_all_ref<A>()

requires

fmt_req_all::<A>(),

ensures

#[trigger] fmt_req_all::<&A>(),