. apply hbackward x (List.Mem.head _)
case mpr.cons.left
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x

case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true