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