suffices ∀ (l : List α) (b : β) (acc : Array β) (h : l.length + (acc.size + 1) = as.length + 1), mapIdx'.go (a :: as) f l ⟨b :: acc.data⟩ h = b :: mapIdx'.go as (f ∘ Fin.succ) l acc (Nat.succ.inj h)
by
  dsimp [mapIdx', mapIdx'.go, Array.push, concat]
  exact this as _ #[] _
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
⊢ mapIdx' (a :: as) f = f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ)
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
⊢ ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)