simp [bind, Except.bind]
case cons
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
hd : τ
tl : List τ
ih :
  List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () tl =
      Except.error () ↔
    ∃ x ∈ tl, f x = true
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () (hd :: tl) =
      Except.error () ↔
    ∃ x ∈ hd :: tl, f x = true
case cons
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
hd : τ
tl : List τ
ih :
  List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () tl =
      Except.error () ↔
    ∃ x ∈ tl, f x = true
⊢ (match if f hd = true then Except.error () else Except.ok () with
      | Except.error err => Except.error err
      | Except.ok v => List.foldlM (fun x x => if f x = true then Except.error () else Except.ok ()) v tl) =
      Except.error () ↔
    f hd = true ∨ ∃ a ∈ tl, f a = true