pub broadcast proof fn lemma_iset_new<A>(f: FnSpec<(A,), bool>, a: A)Expand description
ensures
#[trigger] ISet::new(f).contains(a) == f(a),A call to ISet::new with the predicate f contains a if and only if f(a) is true.