cases Nat.eq_or_lt_of_le i.2 with
| inl heq => cases i; cases heq; exact absurd hi h
| inr hlt => exact Nat.lt_of_succ_lt_succ hlt
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
⊢ ↑i < n
no goals