unfold Fin.elementList
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length (Fin.elementList (Nat.succ n)) = Nat.succ n
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length
      ({ val := 0, isLt := (_ : 0 < Nat.succ n) } ::
        List.map
          (fun x =>
            match x with
            | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
          (Fin.elementList n)) =
    Nat.succ n