proposition: Lemma imap_replace_BoundedIndex {m} {B B' : A -> Type} : forall (f : forall idx'', B idx'' -> B' idx'') (Bound : Vector.t A m) (idx : BoundedIndex Bound) (il : ilist Bound) b, imap f (replace_BoundedIndex il idx b) = replace_BoundedIndex (imap f il) idx (f _ b).
proof: Proof. intros; apply ilist_eq; intros. destruct (BoundedIndex_eq_dec idx idx0); subst; rewrite <- ith_Bounded_imap. - repeat rewrite ith_replace_BoundIndex_eq; reflexivity. - repeat rewrite ith_replace_BoundIndex_neq; auto. rewrite <- ith_Bounded_imap; auto. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2