fact: Fixpoint Iterate_Ensemble_BoundedIndex_filter' ( Remaining : nat) (filter : Fin.t Remaining -> bool) (P : Ensemble (Fin.t Remaining)) {struct Remaining} : Prop := match Remaining return (@Fin.t Remaining -> bool) -> Ensemble (Fin.t Remaining) -> Prop with | 0 => fun filter P => True | S Remaining' => fun filter P => if filter (@Fin.F1 Remaining') then P (@Fin.F1 Remaining') /\ @Iterate_Ensemble_BoundedIndex_filter' Remaining' (fun n' => filter (@Fin.FS _ n')) (fun n' => P (@Fin.FS _ n')) else @Iterate_Ensemble_BoundedIndex_filter' Remaining' (fun n' => filter (@Fin.FS _ n')) (fun n' => P (@Fin.FS _ n')) end filter 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