proposition: Lemma Iterate_Ensemble_equiv'' : forall (Remaining : nat) (P : Ensemble (Fin.t Remaining)), (forall idx, P idx) -> @Iterate_Ensemble_BoundedIndex' Remaining P.
proof: Proof. induction Remaining; simpl; intros; intuition. 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