proposition: Lemma undecidable_PA2_valid : undecidable PA2_valid.
proof: Proof. apply (undecidability_from_reducibility H10p_undec). exists encode_problem. intros e. apply H10p_to_PA2_validity. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.SOL.PA2 Undecidability.SOL.Reductions(H10p_to_SOL) Undecidability.H10(H10p_undec)