Function lemma_iset_finite_if_subset_of_seq Copy item path

pub proof fn lemma_iset_finite_if_subset_of_seq<A>(i: ISet<A>, s: Seq<A>)

forall |a| i.contains(a) ==> s.contains(a),

i.finite(),