Require Import Undecidability.Synthetic.Undecidability.
From Undecidability.CounterMachines
Require Import CM2 Reductions.MM2_HALTING_to_CM2_HALT.
From Undecidability.MinskyMachines
Require Import MM2 MM2_undec.
Lemma CM2_HALT_undec : undecidable CM2_HALT.
Proof.
apply (undecidability_from_reducibility MM2_HALTING_undec).
exact MM2_HALTING_to_CM2_HALT.reduction.
Qed.
Check CM2_HALT_undec.