fact: Fixpoint Iterate_Dep_Type_equiv' (Remaining : nat) (P : Dep_Type (Fin.t Remaining)) (H : @Iterate_Dep_Type_BoundedIndex' Remaining P) idx {struct idx} : P idx := match idx in Fin.t n return forall (P : Dep_Type (Fin.t n)), @Iterate_Dep_Type_BoundedIndex' n P -> P idx with | Fin.F1 i => fun P H => ilist.prim_fst H | Fin.FS i n' => fun P H => Iterate_Dep_Type_equiv' (fun i => P (Fin.FS i)) (ilist.prim_snd H) n' end P H.
imports: Coq.Arith.Arith Coq.Lists.List Coq.Sets.Ensembles Coq.Strings.String Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.DecideableEnsembles