unfold fins.finsAux
case succ
n i : Nat
ih :
  ∀ (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]
hi : Nat.succ i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) (Nat.succ i) ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n (Nat.succ i) hi acc) ++ [Fin.last n]
case succ
n i : Nat
ih :
  ∀ (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]
hi : Nat.succ i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ ({ val := i, isLt := ⋯ } :: (map Fin.castSucc acc ++ [Fin.last n])) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]