conv =>
  lhs; unfold foldlMIdx; unfold foldlMIdx.loop
  rw [dif_neg (by decide : 0 ≠ 0+1)]
  change f 0 init a >>= foldlMIdx.loop f (push empty a) 1 (.refl)
  rhs; ext; unfold foldlMIdx.loop; rw [dif_pos rfl]
case empty
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx f init (push empty a) = do
    let b ← foldlMIdx f init empty
    f 0 b a
case empty
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let x ← f 0 init a
      pure ((_ : 1 = 1) ▸ x)) =
    do
    let b ← foldlMIdx f init empty
    f 0 b a