pub broadcast proof fn lemma_iset_subset_finite<A>(s: ISet<A>, sub: ISet<A>)Expand description
requires
s.finite(),sub.subset_of(s),sub.finite(),A subset of a finite set s is finite.