simp at h_n
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length (remap l f h_f)
⊢ n < length l
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length l
⊢ n < length l