Function vstd::set::fold::lemma_finite_set_induct

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