vstd::set_lib

Function axiom_is_empty_len0

Source 
pub broadcast proof fn axiom_is_empty_len0<A>(s: Set<A>)
Expand description
ensures
#[trigger] s.is_empty() <==> (s.finite() && s.len() == 0),