pub proof fn lemma_map_size<A, B>(x: Set<A>, y: Set<B>, f: FnSpec<(A,), B>)Expand description
requires
injective(f),forall |a: A| x.contains(a) ==> y.contains(#[trigger] f(a)),forall |b: B| (#[trigger] y.contains(b)) ==> exists |a: A| x.contains(a) && f(a) == b,x.finite(),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.