pub broadcast proof fn axiom_mk_map_domain<K, V>(s: Set<K>, f: FnSpec<(K,), V>)
#[trigger] s.mk_map(f).dom() == s,