conv => lhs; unfold fins.finsAux
n : Nat
⊢ fins.finsAux (Nat.succ n) (Nat.succ n) ⋯ [] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
n : Nat
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]