exact dif_pos rfl
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (if h : 0 = 0 then pure (h ▸ init)
    else
      let_fun this := (_ : 0 < 0);
      do
      let __do_lift ← f 0 init empty[0]
      foldlMIdx.loop f empty (0 + 1) this __do_lift) =
    pure init
no goals