rw [← List.foldr_reverse]
case intro.intro
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 α
L : List τ
⊢ (do
      let a ← ma
      List.foldl
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a) L) =
    List.foldl
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma L
case intro.intro
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 α
L : List τ
⊢ (do
      let a ← ma
      List.foldl
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a) L) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma L.reverse