pub broadcast proof fn lemma_set_complement<A>(s: Set<A>, a: A)Expand description
requires
ISet::new(|a| !s.contains(a)).finite(),#[trigger] s.complement().unwrap().contains(a) == !s.contains(a),The complement of set s contains element a if and only if s does not contain a.