simp only [mapIdx'_cons]
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : i < length (mapIdx' (a :: as) f)
⊢ (mapIdx' (a :: as) f)[i] = f { val := i, isLt := (_ : i < length (a :: as)) } (a :: as)[i]
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : i < length (mapIdx' (a :: as) f)
⊢ (f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ))[i] =
    f { val := i, isLt := (_ : i < length (a :: as)) } (a :: as)[i]