pub broadcast proof fn lemma_iset_contains_len<A>(s: ISet<A>, a: A)Expand description
requires
s.finite(),#[trigger] s.contains(a),#[trigger] s.len() != 0,If a finite set s contains any element, it has length greater than 0.