proposition: Lemma mm2_steps_not_terminates_l {P x y} : P // x ↠ y -> not (P // y ↓) -> not (P // x ↓).
proof: Proof. move=> Hxy Hy Hx. apply: Hy. by apply: mm2_steps_terminates_r; eassumption. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun