apply bind_congr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ (do
      let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (n✝ + 1)) } a
      let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
      pure (cons b y)) =
    do
    let x_1 ← f { val := 0, isLt := (_ : ↑{ val := 0, isLt := (_ : 0 < Nat.succ n✝) } < Nat.succ (n✝ + 1)) } a
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons x_1 (push x b))
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ ∀ (a : β),
    (do
        let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
        pure (cons a y)) =
      do
      let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
      let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
      pure (cons a (push x b))