cases i with | mk i h => rfl
case h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
i : Fin n
⊢ ((fun i => f (cons a x)[i]) ∘ Fin.succ) i = f x[i]
no goals