case succ n h_ind => unfold Fin.elementList; unfold List.length; rw [List.length_map, h_ind]
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length (Fin.elementList (Nat.succ n)) = Nat.succ n
no goals