Function vstd::set::axiom_set_intersect_finite

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

The intersection of two finite sets is finite.