proposition: Lemma CM1_HALT_undec : undecidable CM1_HALT.
proof: Proof. apply (undecidability_from_reducibility MM2_HALTING_undec). exact MM2_HALTING_to_CM1_HALT.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.CounterMachines.CM1 Undecidability.CounterMachines.Reductions.MM2_HALTING_to_CM1_HALT Undecidability.MinskyMachines.MM2_undec