apply h
case a.a
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ n < length l
no goals