suffices ∀ (i j) (h : i + j = x.size) (y : Array β), mapIdxM.map x f' i j h (cons b y) = (mapIdxM.map x f' i j h y >>= λ y => pure (cons b y))
from this x.size 0 rfl #[]
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ ∀ (i j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)