pub broadcast proof fn lemma_set_new<A>(f: FnSpec<(A,), bool>, a: A)Expand description
requires
Set::<A>::new(f) is Some,#[trigger] Set::<A>::new(f).unwrap().contains(a) == f(a),If Set::<A>::new(f) produces Some(s), then s contains a
if and only if f(a) is true.