exact this
n : Nat
this✝ : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
this : length (fins.finsAux n n ⋯ []) = n
⊢ length (fins.finsAux n n ⋯ []) = n
no goals