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),#[trigger] s.mk_map(f)[key] == f(key),