pub broadcast proof fn lemma_set_filter<A>(s: Set<A>, f: FnSpec<(A,), bool>, a: A)Expand description
ensures
#[trigger] s.filter(f).contains(a) == (s.contains(a) && f(a)),The filter of set s using function f contains element a if and only if s contains a
and f(a) is true.