proposition: Lemma Iterate_Ensemble_equiv_filter' : forall (Remaining : nat) (P : Ensemble (Fin.t Remaining)) (filter : Ensemble (Fin.t Remaining)) (filter_dec : DecideableEnsemble filter), (@Iterate_Ensemble_BoundedIndex_filter' Remaining (@dec _ _ filter_dec) P -> forall idx, filter idx -> P idx).
proof: Proof. induction Remaining; simpl; intros. - inversion idx. - revert IHRemaining filter filter_dec P H H0. pattern Remaining, idx; apply Fin.caseS; intros. + apply dec_decides_P in H0; rewrite H0 in H. intuition. + assert (forall a : Fin.t n, dec (Fin.FS a) = true <-> dec (Fin.FS a)) as decOK by intuition. case_eq (dec Fin.F1); intros; rewrite H1 in H; intuition; eapply dec_decides_P in H0. eapply (IHRemaining (fun n' : Fin.t n => P (Fin.FS n')) (fun n' : Fin.t n => dec (Fin.FS n')) {| dec n' := dec (Fin.FS n'); dec_decides_P := decOK |} prim_snd0); eauto. eapply (IHRemaining (fun n' : Fin.t n => P (Fin.FS n')) (fun n' : Fin.t n => dec (Fin.FS n')) {| dec n' := dec (Fin.FS n'); dec_decides_P := decOK |} H); eauto. 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