proposition: Lemma mm2_steps_terminates_l {P x y} : P // x ↠ y -> P // y ↓ -> P // x ↓.
proof: Proof. move=> Hxy [z] [Hyz Hz]. exists z. split; [|done]. by apply: rt_trans; eassumption. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun