Require Import Undecidability.Synthetic.Definitions.

Require Import Undecidability.MinskyMachines.MM.
From Undecidability.MinskyMachines.Deciders Require
  MM_2_HALTING_dec.

Theorem MM_2_HALTING_dec : decidable MM_2_HALTING.
Proof.
  exists MM_2_HALTING_dec.decide.
  exact MM_2_HALTING_dec.decide_spec.
Qed.

Check MM_2_HALTING_dec.