rfl
case refl
α : Type u
n : Nat
f✝ : Fin n → α
i : Nat
IH : ∀ (x : Fin i → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < i) }
f : Fin (Nat.succ i) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ i) })
⊢ f { val := i, isLt := (_ : i < Nat.succ i) } = f { val := i, isLt := (_ : i < Nat.succ i) }
no goals