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