vstd::set

Function 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,