pub proof fn lemma_map_size<A, B>(x: Set<A>, y: Set<B>, f: FnSpec<(A,), B>)Expand description
requires
x.finite(),injective_on(f, x),x.map(f) == y,y.finite(),x.len() == y.len(),If an injective function is applied to each element of a set to construct another set, the two sets have the same size.