simp [foldr] at hforward
case mp.head
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x : α
as : List α
hforward : foldr (fun a r => decide (p a) && r) true (x :: as) = true
⊢ p x
case mp.head
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x : α
as : List α
hforward : p x ∧ foldr (fun a r => decide (p a) && r) true as = true
⊢ p x