Function lemma_iset_mk_map_domain Copy item path

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

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