proposition: Lemma Halt_murec_undec : undecidable Halt_murec.
proof: Proof. apply (undecidability_from_reducibility H10_undec). eapply H10_MUREC_HALTING. Qed.
imports: Undecidability.MuRec.MuRec Undecidability.H10.H10 Undecidability.MuRec.Reductions.H10_to_MUREC_HALTING Undecidability.H10.H10_undec Undecidability.Synthetic.Undecidability