simp_all [pure, Except.pure]
case nil
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
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () [] =
      Except.error () ↔
    ∃ x ∈ [], f x = true
no goals