pub broadcast proof fn lemma_set_new_some<A>(f: FnSpec<(A,), bool>)Expand description
requires
ISet::<A>::new(f).finite(),#[trigger] Set::<A>::new(f) is Some,If ISet::<A>::new(f) is finite, then Set::<A>::new(f)
produces Some(s). Useful for triggering the lemma_set_new
to show that s contains a if and only if f(a) is true.