pub proof fn lemma_map_size_bound<A, B>(x: Set<A>, y: Set<B>, f: FnSpec<(A,), B>)Expand description
requires
x.finite(),x.map(f) == y,y.finite(),y.len() <= x.len(),If any function is applied to each element of a set to construct another set, the constructed set’s length is at most the original’s