cases Nat.eq_or_lt_of_le hi₂ with
| inl heq =>
  cases heq; unfold loop; simp only [dif_pos]; rw [pure_bind]
| inr hlt =>
  unfold loop
  simp only [Nat.ne_of_lt hlt, Nat.ne_of_lt (Nat.succ_lt_succ hlt), dif_neg]
  rw [bind_assoc]
  apply bind_congr; intro b'
  rw [push_cons_eq_cons_push]
  exact mapMIdx.loop_cons_succ f a x (i+1) b (push r b')
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop (f ∘ Fin.succ) x i hi₂ r
    pure (cons b y)
no goals