simp
case intro.intro.cons
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 τ
hd : τ
tl : List τ
ih :
  (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) tl) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma tl
⊢ (do
      let x ← ma
      let acc ←
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
      f acc hd) =
    do
    let acc ←
      do
        let x ← ma
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
    f acc hd
no goals