proposition: Lemma Iterate_Dep_Type_equiv_filter'' : forall (Remaining : nat) (P : Dep_Type (Fin.t Remaining)) (filter : Ensemble (Fin.t Remaining)) (filter_dec : DecideableEnsemble filter), (forall idx, filter idx -> P idx) -> @Iterate_Dep_Type_BoundedIndex_filter' Remaining (@dec _ _ filter_dec) P.
proof: Proof. induction Remaining; simpl; intros. - eauto. - case_eq (dec Fin.F1); intros. + apply dec_decides_P in H; intuition. assert (forall a : Fin.t Remaining, dec (Fin.FS a) = true <-> dec (Fin.FS a)) as decOK by intuition. eapply (IHRemaining (fun n' : Fin.t _ => P (Fin.FS n')) (fun n' : Fin.t _ => dec (Fin.FS n')) {| dec n' := dec (Fin.FS n'); dec_decides_P := decOK |}); eauto. intros; eapply X; apply dec_decides_P; eauto. + assert (forall a : Fin.t Remaining, dec (Fin.FS a) = true <-> dec (Fin.FS a)) as decOK by intuition. eapply (IHRemaining (fun n' : Fin.t _ => P (Fin.FS n')) (fun n' : Fin.t _ => dec (Fin.FS n')) {| dec n' := dec (Fin.FS n'); dec_decides_P := decOK |}); eauto. intros; eapply X; apply dec_decides_P; eauto. Defined.
imports: Coq.Arith.Arith Coq.Lists.List Coq.Sets.Ensembles Coq.Strings.String Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.DecideableEnsembles