Function vstd::set::axiom_set_empty_finite

pub broadcast proof fn axiom_set_empty_finite<A>()

Expand description

ensures

#[trigger] Set::<A>::empty().finite(),

The empty set is finite.