Function axiom_mk_map_indexCopy item path

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

s.contains(key),

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