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