proposition: Lemma ith_replace2_Index_eq {m} : forall (n : Fin.t m) (As : Vector.t A m) (il : ilist2 As) (new_b : B (Vector.nth As n)), ith2 (replace_Index2 As il n new_b) n = new_b.
proof: Proof. induction n; simpl. - intro As; pattern n, As. match goal with |- ?P n As => simpl; apply (@Vector.caseS _ P); intros; reflexivity end. - intro As; revert n0 IHn; pattern n, As. match goal with |- ?P n As => simpl; apply (@Vector.caseS _ P); simpl; eauto end. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common Fiat.Common.VectorFacts