proposition: Lemma imap_replace2_BoundedIndex {m} {B B' : A -> Type} : forall (f : forall idx'', B idx'' -> B' idx'') (Bound : Vector.t A m) (idx : BoundedIndex Bound) (il : ilist2 Bound) b, imap2 f (replace_BoundedIndex2 il idx b) = replace_BoundedIndex2 (imap2 f il) idx (f _ b).
proof: Proof. intros; apply ilist2_eq; intros. destruct (BoundedIndex_eq_dec idx idx0); subst; rewrite <- ith_Bounded_imap2. - repeat rewrite ith_replace_BoundIndex2_eq; reflexivity. - repeat rewrite ith_replace_BoundIndex2_neq; auto. rewrite <- ith_Bounded_imap2; auto. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2