fact: Definition ith_Bounded {m} {B : A -> Type} {Bound : Vector.t A m} (il : ilist Bound) (idx : BoundedIndex Bound) : B (Vector.nth Bound (ibound (indexb idx))) := ith il (ibound (indexb idx)) .
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2