Function vstd::set::axiom_set_union_finite

source · 
pub broadcast proof fn axiom_set_union_finite<A>(s1: Set<A>, s2: Set<A>)
Expand description
requires
s1.finite(),
s2.finite(),
ensures
#[trigger] s1.union(s2).finite(),

The union of two finite sets is finite.