refine .intro (l.pmap (fun i (hi : i.1 < n) => ⟨i.1,hi⟩) ?_) ?_
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∃ l', l = List.map castSucc l'
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (a : Fin (n + 1)), a ∈ l → ↑a < n

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 ?refine_1)