pub broadcast proof fn axiom_set_contains_len<A>(s: Set<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.