Function lemma_iset_is_empty_len0 Copy item path

pub broadcast proof fn lemma_iset_is_empty_len0<A>(s: ISet<A>)

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