rfl
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = ((x :: δ).get ⟨↑⟨↑i, h⟩, ⋯⟩, (X :: (l ++ [Y])).get ⟨↑⟨↑i, h⟩, ⋯⟩).2
no goals