intro a as
σ : 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 γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
⊢ ∀ (a : α) (b : List α), List.foldr (fun a' ih => a == a' || ih) false b = decide ((fun x x_1 => x ∈ x_1) a b)
σ : 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 γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a : α
as : List α
⊢ List.foldr (fun a' ih => a == a' || ih) false as = decide ((fun x x_1 => x ∈ x_1) a as)