proposition: Lemma Iterate_Ensemble_equiv' : forall (Remaining : nat) (P : Ensemble (Fin.t Remaining)), (@Iterate_Ensemble_BoundedIndex' Remaining P -> forall idx, P idx).
proof: Proof. induction Remaining; simpl; intros. - inversion idx. - revert IHRemaining P H. pattern Remaining, idx; apply Fin.caseS; intros. + intuition. + intuition; eapply (IHRemaining _ prim_snd0). 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