Function vstd::set::axiom_mk_map_index

source · 
pub broadcast proof fn axiom_mk_map_index<K, V>(s: Set<K>, f: FnSpec<(K,), V>, key: K)
Expand description
requires
s.contains(key),
ensures
#[trigger] s.mk_map(f)[key] == f(key),