proposition: Lemma mm2_sig_step_dec P x : { y | mm2_step P x y } + { forall y, not (mm2_step P x y) }.
proof: Proof. move: x => [[|i] [a b]]. { right => y [?] /= [] [?] [?]. lia. } case Hinstr: (nth_error P i) => [instr|]. + left. have [y Hxy] := mm2_progress instr (S i, (a, b)). exists y. exists instr. by split; [apply /nth_error_Some_mm2_instr_at_iff|]. + right => y [?] /= [/nth_error_Some_mm2_instr_at_iff]. by rewrite Hinstr. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun