fact: Fixpoint Iterate_Ensemble_BoundedIndex' (Remaining : nat) (P : Ensemble (Fin.t Remaining)) {struct Remaining} : Prop := match Remaining return Ensemble (Fin.t Remaining) -> Prop with | 0 => fun P => True | S Remaining' => fun P => P (@Fin.F1 Remaining') /\ @Iterate_Ensemble_BoundedIndex' Remaining' (fun n' => P (@Fin.FS _ n')) end P.
imports: Coq.Arith.Arith Coq.Lists.List Coq.Sets.Ensembles Coq.Strings.String Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.DecideableEnsembles