rw [List.length_map, List.length_pmap]
case refine_2.hl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ List.length l =
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
no goals