Require Import Undecidability.Synthetic.Definitions.

From Undecidability.MinskyMachines Require Import MM MM_sss.
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.