proposition: Lemma ith_Bounded_imap {m} {B B' : A -> Type} : forall (f : forall idx, B idx -> B' idx) (Bound : Vector.t A m) (idx : BoundedIndex Bound) (il : ilist Bound), f _ (ith_Bounded il idx) = ith_Bounded (imap _ _ f Bound il) idx.
proof: Proof. unfold ith_Bounded; simpl; intros; eapply ith_imap. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2