apply extF <;> simp
α : Type u_1
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
h_g : ∀ (n : ℕ), n < length (remap l f h_f) → g n < length (remap l f h_f)
⊢ remap (remap l f h_f) g h_g = remap l (f ∘ g) (_ : ∀ (n : ℕ), n < length l → Function.comp f g n < length l)
no goals