proposition: Corollary Iterate_Ensemble_BoundedIndex_filter_equiv : forall (Bound : nat) (P : Ensemble (Fin.t Bound)) (filter : Ensemble (Fin.t Bound)) (filter_dec : DecideableEnsemble filter), Iterate_Ensemble_BoundedIndex_filter P dec <-> forall idx : Fin.t Bound, filter idx -> P idx.
proof: Proof. split; intros. - eapply Iterate_Ensemble_equiv_filter'; eauto using string_dec; destruct n; simpl; discriminate. - eapply Iterate_Ensemble_equiv_filter'' ; eauto using string_dec. Qed.
imports: Coq.Arith.Arith Coq.Lists.List Coq.Sets.Ensembles Coq.Strings.String Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.DecideableEnsembles