induction n
n : Nat
⊢ List.length (Fin.elementList n) = n
case zero

⊢ List.length (Fin.elementList Nat.zero) = Nat.zero

case succ
n✝ : Nat
n_ih✝ : List.length (Fin.elementList n✝) = n✝
⊢ List.length (Fin.elementList (Nat.succ n✝)) = Nat.succ n✝