apply list_mem.comp₂
  (by apply list_cons.comp₂
        (by apply Semiformula.substs₁_primrec.comp₂ (snd.comp₂ Primrec₂.right) (fst.comp₂ Primrec₂.right))
        (by apply fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left))
  (snd.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide ([→ val.2].hom val.1 :: p.1.1.1.1.1.1.1 ∈ p.1.1.1.1.1.1.2)
no goals