intro l₁ l₂
σ : 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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
⊢ ∀ (a b : List α), List.foldr (fun a' ih => decide (a' ∈ b) && ih) true a = 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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
l₁ l₂ : List α
⊢ List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁ = decide ((fun x x_1 => x ⊆ x_1) l₁ l₂)