proposition: Lemma ith_replace_Index_neq {m} : forall (n n' : Fin.t m) (As : Vector.t A m) (il : ilist As) (new_b : B (Vector.nth As n')), n <> n' -> ith (replace_Index As il n' new_b) n = ith il n.
proof: Proof. intros n n'; pattern m, n, n'. match goal with |- ?P m n n' => simpl; eapply (Fin.rect2 P); intros end. - congruence. - generalize il f new_b; clear f new_b il H. pattern n0, As. match goal with |- ?P n0 As => simpl; apply (@Vector.rectS _ P); intros; reflexivity end. - generalize il f new_b; clear f new_b il H. pattern n0, As. match goal with |- ?P n0 As => simpl; apply (@Vector.rectS _ P); intros; reflexivity end. - assert (f <> g) by congruence. generalize il f g new_b H H1; clear f g new_b il H H1 H0. pattern n0, As. match goal with |- ?P n0 As => simpl; apply (@Vector.caseS _ P); intros; eapply (H _ (prim_snd il) new_b); eauto end. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common Fiat.Common.VectorFacts