proposition: Theorem undecidable_ext_entailment_PA : undecidable ext_entailment_PA.
proof: Proof. refine (undecidability_from_reducibility _ H10_to_ext_entailment_PA). apply H10p_undec. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.FOL.PA Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Deduction.FullNDFacts Semantics.Tarski.FullSoundness) Undecidability.H10(H10p_undec) Undecidability.FOL.Reductions(H10p_to_FA)