proposition: Lemma i2th_replace_Index_neq : forall {m : nat} {As : Vector.t A m} {Bs : ilist2 As} (i2l : i2list C Bs) (n n' : Fin.t m) (new_c : C (ith2 Bs n)), n <> n' -> i2th (replace2_Index2 i2l n new_c) n' = i2th i2l n'.
proof: Proof. induction As. - intros; inversion n. - intros; revert n' As Bs i2l new_c H IHAs; pattern n, n0. match goal with |- ?P n n0 => simpl; apply (@Fin.caseS P); clear n n0; simpl in * end. + intros n n'; pattern n, n'; match goal with |- ?P n n' => simpl; apply (@Fin.caseS P); clear n n'; intros; simpl in *; eauto; congruence end. + intros n p n'; revert p; pattern n, n'; match goal with |- ?P n n' => simpl; apply (@Fin.caseS P); clear n n'; intros; simpl in *; eauto end. eapply IHAs; congruence. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common.ilist2