apply ih
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : foldr (fun a r => decide (p a) && r) true (a :: as✝) = true
⊢ p x
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : foldr (fun a r => decide (p a) && r) true (a :: as✝) = true
⊢ foldr (fun a r => decide (p a) && r) true as✝ = true