Skip to main content

lemma_set_is_empty

vstd::set_lib

Function lemma_set_is_empty 

Source 
pub broadcast proof fn lemma_set_is_empty<A>(s: Set<A>)
Expand description
requires
!(#[trigger] s.is_empty()),
ensures
exists |a: A| s.contains(a),