Theorem: LO.FirstOrder.isProofFn_computable (Logic/FirstOrder/Computability/Calculus.lean)

State before:
μ : Type ?u.1302484
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 μ
T : Theory L
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ Primrec fun p => decide (List.map (⇑Rew.emb.hom) (p.1.1 :: List.map (fun x => ~x) p.2.2) ∈ p.2.1.sequents)
Tactic:
apply Primrec.list_mem.comp
  (Primrec.list_map
    (Primrec.list_cons.comp (Primrec.fst.comp .fst)
      (Primrec.list_map (Primrec.snd.comp .snd) $ Semiformula.neg_primrec.comp₂ .right))
      <| Semiformula.emb_primrec.comp₂ .right)
  (Primrec.list_map (Primrec.fst.comp .snd) <| Primrec.snd.comp₂ .right)
State after:
no goals