congr
case refl
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
h : n < size (init (Nat.succ n) f)
h' : n ≤ n
⊢ f { val := n, isLt := ⋯ } = f { val := n, isLt := ⋯ }
no goals