suffices ∀ i (hi : i ≤ n) acc,
    fins.finsAux n.succ i (trans hi (Nat.le_succ _)) (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
  by have := this n (Nat.le_refl _) []; simpa using this
n : Nat
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
n : Nat
⊢ ∀ (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]