proposition: Corollary Iterate_Ensemble_BoundedIndex_equiv : forall m (P : Ensemble (Fin.t m)), Iterate_Ensemble_BoundedIndex P <-> forall idx, P idx.
proof: Proof. split; intros. eapply Iterate_Ensemble_equiv'; eauto using string_dec; destruct n; simpl; discriminate. eapply Iterate_Ensemble_equiv''; 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