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