have := ToList.fold_eq_fold_toList c
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
⊢ (do
      let a ← ma
      fold c
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a)) =
    fold c
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
this : ∃ L, L.Perm (toList c) ∧ ∀ {β : Type u_2} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ (do
      let a ← ma
      fold c
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a)) =
    fold c
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma