Function vstd::set::axiom_set_empty_len

source · 
pub broadcast proof fn axiom_set_empty_len<A>()
Expand description
ensures
#[trigger] Set::<A>::empty().len() == 0,

The empty set has length 0.