. intros hbackward
  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 α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
no goals