pub broadcast proof fn lemma_set_new_assuming_finite<A>(f: FnSpec<(A,), bool>, a: A)Expand description
ensures
#[trigger] Set::<A>::new_assuming_finite(f).contains(a) == f(a),Shows that Set::<A>::new_assuming_finite(f) contains a
if and only if f(a) is true.