proposition: Lemma mm2_exists_step_dec P x : (exists y, mm2_step P x y) \/ (forall y, not (mm2_step P x y)).
proof: Proof. have [[y Hy]|Hx] := mm2_sig_step_dec P x. - left. by exists y. - by right. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun