no goals
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
a : α
⊢ mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l
simp [mapIdx_eq_enum_map, enum_eq_zip_range, map_uncurry_zip_eq_zipWith,
  range_succ_eq_map, zipWith_map_left]