Function lemma_empty_bad_set_implies_forall

pub proof fn lemma_empty_bad_set_implies_forall<T>(
    p: FnSpec<(T,), bool>,
    q: FnSpec<(T,), bool>,
)

Expand description

requires

Set::new(|x: T| p(x)).filter(|x| !q(x)).is_empty(),

ensures

forall |x: T| #[trigger] p(x) ==> q(x),

If no element in set Set::new(|x: T| p(x)) satisfies the predicate q, then all elements satisfying p also satisfy q.

lemma_empty_bad_set_implies_forall