proposition: Lemma mm2_steps_stop_refl {P x y} : P // x ↠ y -> mm2_stop P x -> y = x.
proof: Proof. move=> /clos_rt_rt1n_iff []; [done|]. by move=> > + _ H => /H. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun