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