dsimp [mapIdxM.map]
case h.zero
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
j : Nat
h : Nat.zero + j = size x
y : Array β
⊢ mapIdxM.map x f' Nat.zero j h (cons b y) = do
    let y ← mapIdxM.map x f' Nat.zero j h y
    pure (cons b y)
case h.zero
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
j : Nat
h : Nat.zero + j = size x
y : Array β
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)