proposition: Theorem RA_UNIV_HALT_undec : undecidable RA_UNIV_HALT.
proof: Proof. apply (undecidability_from_reducibility H10C_SAT_undec). exact H10C_SAT_to_RA_UNIV_HALT.H10C_SAT_RA_UNIV_HALT. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.MuRec.Util.RA_UNIV_HALT Undecidability.DiophantineConstraints.H10C_undec