Function lemma_full_good_set_implies_forall

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

Expand description

requires

Set::new(|x: T| p(x)).finite(),

Set::new(|x: T| p(x)).len() == Set::new(|x: T| p(x)).filter(q).len(),

ensures

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

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

lemma_full_good_set_implies_forall