rw [eq_comm]
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'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
⊢ (match foldM c f' () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false) =
    (toList c).all f
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'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
⊢ (toList c).all f =
    match foldM c f' () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false