Function vstd::set_lib::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),