intro i hi
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_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
⊢ ↑i < n