have : Primrec₂ (fun l₁ l₂ => l₁.foldr (fun a' ih => a' ∈ l₂ && ih) true : List α → List α → Bool) :=
  to₂' <| list_foldr fst (const true)
    <| (dom_bool₂ _).comp₂
      (list_mem.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.left))
      (snd.comp₂ Primrec₂.right)
σ : 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 α
⊢ PrimrecRel fun x x_1 => x ⊆ x_1
σ : 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₁
⊢ PrimrecRel fun x x_1 => x ⊆ x_1