proposition: Corollary Lookup_Iterate_Dep_Type : forall m (P : Dep_Type (Fin.t m)), Iterate_Dep_Type_BoundedIndex P -> forall idx, P idx.
proof: Proof. intros; eapply Iterate_Dep_Type_equiv' ; 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