pub proof fn lemma_full_good_set_implies_forall<T>(s: Set<T>, q: FnSpec<(T,), bool>)Expand description
requires
s.len() == s.filter(q).len(),forall |x: T| #[trigger] s.contains(x) ==> q(x),If all elements in the set s satisfy predicate q (i.e., the filtered set has the same length),
then every element of s satisfies q.