simp [remap]
α : Type u_1
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length (remap l f h_f)
⊢ getF (remap l f h_f) n h_n = getF l (f n) (_ : f n < length l)
no goals