pub broadcast proof fn lemma_iset_intersect_finite<A>(s1: ISet<A>, s2: ISet<A>)Expand description
requires
s1.finite() || s2.finite(),#[trigger] s1.intersect(s2).finite(),The intersection of two finite sets is finite.