proposition: Corollary Lookup_Iterate_Dep_Type_filter : forall (Bound : nat) (P : Dep_Type (Fin.t Bound)) (filter : Ensemble (Fin.t Bound)) (filter_dec : DecideableEnsemble filter), Iterate_Dep_Type_BoundedIndex_filter P dec -> forall idx : Fin.t Bound, filter idx -> P idx.
proof: Proof. intros. eapply Iterate_Dep_Type_equiv_filter' ; eassumption. 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