apply bind_congr
case h.succ
α : 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 : Nat
IH :
  ∀ (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)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ (do
      let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
      mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) __do_lift)) =
    do
    let x_1 ← f' { val := j, isLt := (_ : j < size x) } x[j]
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y x_1)
    pure (cons b y)
case h.succ.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 : Nat
IH :
  ∀ (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)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ ∀ (a : β),
    mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) a) = do
      let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y a)
      pure (cons b y)