induction i generalizing acc with
| zero => unfold fins.finsAux; simp
| succ i ih =>
  unfold fins.finsAux
  replace ih := ih (Nat.le_of_lt hi) (⟨i,hi⟩ :: acc)
  simpa using ih
n i : Nat
hi : i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
no goals