rw [h]
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ fold c
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) =
      Except.ok () ↔
    (toList c).all f = true
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    (toList c).all f = true