rw [bind_pure]
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)) =
    f 0 init a
no goals