Replacing consecutive entries of a list

The lists u ++ a :: v and u ++ a' :: v differ at most in the position u.length, and the lists u ++ a :: b :: c :: v and u ++ a' :: b' :: c' :: v differ at most in the three positions u.length, u.length + 1 and u.length + 2. They agree at every other position.

theorem List.getElem?_append_cons_of_ne {α : Type u_1} (u v : List α) (a a' : α) {k : ℕ} (h : k ≠ u.length) : (u ++ a :: v)[k]? = (u ++ a' :: v)[k]?

Two lists which differ only in the entry following u have the same entry at every other position.

theorem List.getElem?_append_cons_cons_cons_of_ne {α : Type u_1} (u v : List α) (a b c a' b' c' : α) {k : ℕ} (h₀ : k ≠ u.length) (h₁ : k ≠ u.length + 1) (h₂ : k ≠ u.length + 2) : (u ++ a :: b :: c :: v)[k]? = (u ++ a' :: b' :: c' :: v)[k]?

Two lists which differ only in the three entries following u have the same entry at every other position.