no goals
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
i : ℕ
h : i < length l
h' : optParam (i < length (mapIdx f l)) (_ : i < length (mapIdx f l))
⊢ nthLe (mapIdx f l) i h' = f i (nthLe l i h)
simp [mapIdx_eq_enum_map, enum_eq_zip_range]