induction hx with
| head as =>
  simp [foldr] at hforward
  apply And.left hforward
| tail a h ih =>
  apply ih
  simp [foldr] at hforward
  apply And.right hforward
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hforward : foldr (fun a r => decide (p a) && r) true xs = true
x : α
hx : x ∈ xs
⊢ p x
no goals