pub broadcast proof fn axiom_set_empty_finite<A>()Expand description
ensures
#[trigger] Set::<A>::empty().finite(),The empty set is finite.
pub broadcast proof fn axiom_set_empty_finite<A>()#[trigger] Set::<A>::empty().finite(),The empty set is finite.