Church theorem general

theorem church_theorem_general : ¬ComputablePred T.theory := by  by_contra hC  have hQuoteSubst :      Computable₂ fun σ π : ArithmeticSemisentence 1 ↦ (σ/[⌜π⌝] : ArithmeticSentence) :=    computable₂_iff_sigma1_simulate (f := substNumeral (V := ℕ)) (by definability)      fun σ τ ↦ by simp [←Sentence.quote_eq_encode_nat, substNumeral_app_quote]  have hSubst : Computable fun σ : ArithmeticSemisentence 1 ↦ (σ/[⌜σ⌝] : ArithmeticSentence) :=    hQuoteSubst.comp Computable.id Computable.id  have hD : ComputablePred (fun σ : ArithmeticSemisentence 1 ↦ T ⊬ σ/[⌜σ⌝]) :=    ComputablePred.computable_of_manyOneReducible      (ManyOneReducible.mk (fun σ ↦ T ⊬ σ) hSubst) hC.not  let D : ℕ → Prop :=    fun n ↦ (Encodable.decode (α := ArithmeticSemisentence 1) n).elim False      (fun σ ↦ T ⊬ σ/[⌜σ⌝])  have hRe : REPred D := by    simpa [D] using REPred.iff_decoded_pred.mp hD.to_re  have hδ : T ⊬ (codeOfREPred D)/[⌜codeOfREPred D⌝] ↔      T ⊢ (codeOfREPred D)/[⌜codeOfREPred D⌝] := by    simpa [D, Encodable.encodek, Arithmetic.gödelNumber'_eq_coe_encode]      using rePred_weak_representation (T := T) hRe (x := Encodable.encode (codeOfREPred D))  tauto