suffices ∀ i (hi : i ≤ n) acc, length (fins.finsAux n i hi acc) = length acc + i
  by have := this n (Nat.le_refl _) []; simp at this; exact this
n : Nat
⊢ length (fins.finsAux n n ⋯ []) = n
n : Nat
⊢ ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i