induction xs with
| nil => simp [foldr]
| cons x xs ih =>
  simp [foldr]
  apply And.intro
  . apply hbackward x (List.Mem.head _)
  . apply ih
    intro x' hx'
    apply hbackward _ $ List.Mem.tail _ hx'
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hbackward : ∀ (x : α), x ∈ xs → p x
⊢ foldr (fun a r => decide (p a) && r) true xs = true
no goals