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