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