pub proof fn lemma_finite_set_induct<A>(s: ISet<A>, pred: FnSpec<(ISet<A>,), bool>)Expand description
requires
s.finite(),pred(ISet::empty()),forall |s, a| pred(s) && s.finite() && !s.contains(a) ==> #[trigger] pred(s.insert(a)),pred(s),