proposition: Lemma decide_spec : decider decide MPM2_HALT.
proof: Proof. rewrite /decider /reflects /decide => - [M c]. case: (decision M c). - tauto. - move=> H. split; [by move=> [k /H] | done]. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions