dsimp [mapIdx'.go]
case nil
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
acc : Array β
h : length [] + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f [] { data := b :: acc.data } h =
    b :: mapIdx'.go as (f ∘ Fin.succ) [] acc (_ : length [] + Array.size acc = length as)
case nil
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
acc : Array β
h : length [] + (Array.size acc + 1) = length as + 1
⊢ Array.toList { data := b :: acc.data } = b :: Array.toList acc