pub broadcast proof fn lemma_iset_difference_finite<A>(s1: ISet<A>, s2: ISet<A>)Expand description
requires
s1.finite(),#[trigger] s1.difference(s2).finite(),The set difference between two finite sets is finite.