unfold fins.finsAux
case succ
n n✝ : Nat
n_ih✝ : ∀ (hi : n✝ ≤ n) (acc : List (Fin n)), length (fins.finsAux n n✝ hi acc) = length acc + n✝
hi : Nat.succ n✝ ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n (Nat.succ n✝) hi acc) = length acc + Nat.succ n✝
case succ
n n✝ : Nat
n_ih✝ : ∀ (hi : n✝ ≤ n) (acc : List (Fin n)), length (fins.finsAux n n✝ hi acc) = length acc + n✝
hi : Nat.succ n✝ ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n n✝ ⋯ ({ val := n✝, isLt := hi } :: acc)) = length acc + Nat.succ n✝