proposition: Lemma ith_replace_BoundIndex2_eq {m} {B : A -> Type} : forall (Bound : Vector.t A m) (il : ilist2 Bound) (idx : BoundedIndex Bound) (new_b : B (nth_Bounded idx)), ith_Bounded2 (replace_BoundedIndex2 il idx new_b) idx = new_b.
proof: Proof. unfold ith_Bounded2; simpl; intros; eapply ith_replace2_Index_eq. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2