induction bs <;> simp[*]
σ : Type u_1
α✝ : Type u_2
β✝ : α✝ → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α✝
inst✝⁶ : (a : α✝) → Fintype (β✝ a)
inst✝⁵ : (a : α✝) → DecidableEq (β✝ a)
inst✝⁴ : (a : α✝) → Primcodable (β✝ a)
inst✝³ : PrimrecCard β✝
inst✝² : Primcodable γ
α : Type u_5
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
a : α
bs : List β
⊢ List.foldr (fun b s => p a b && s) true bs = bs.all (p a)
no goals