Function lemma_set_is_empty_len0 Copy item path

pub broadcast proof fn lemma_set_is_empty_len0<A>(s: Set<A>)

#[trigger] s.is_empty() <==> s.len() == 0,