no goals
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i✝ : Fin n
y✝ : α (succ i✝)
z x₀ y₀ : α 0
x y : (i : Fin n) → α (succ i)
h : cons x₀ x = cons y₀ y
i : Fin n
⊢ x i = y i
simpa using congr_fun h (Fin.succ i)