Function vstd::set::axiom_mk_map_domain
source · pub broadcast proof fn axiom_mk_map_domain<K, V>(s: Set<K>, f: FnSpec<(K,), V>)Expand description
ensures
#[trigger] s.mk_map(f).dom() == s,