Function lemma_iset_mk_map_index Copy item path

pub broadcast proof fn lemma_iset_mk_map_index<K, V>(s: ISet<K>, f: FnSpec<(K,), V>, key: K)

s.contains(key),

#[trigger] s.mk_map(f)[key] == f(key),