proposition: Lemma decide_spec : decider decide MM2_REV.
proof: Proof. rewrite /decider /reflects /decide => M. case: (decision M); [tauto | done]. Qed.
imports: List ListDec PeanoNat Lia Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions