apply hbackward _ $ List.Mem.tail _ hx'
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
x' : α
hx' : x' ∈ xs
⊢ p x'
no goals