pub proof fn lemma_empty_bad_set_implies_forall<T>(s: Set<T>, q: FnSpec<(T,), bool>)Expand description
requires
s.filter(|x| !q(x)).is_empty(),forall |x: T| #[trigger] s.contains(x) ==> q(x),If no element in set s fails the predicate q, then all elements in s satisfy q.