proposition: Lemma steps'_incl k x y : steps' k x = Some y -> reaches x y.
proof: Proof. elim: k y. { move=> y /= [<-]. by apply: rt_refl. } move=> k /=. case: (steps' k x) => [y|]; last done. move=> /(_ y erefl) /= Hxy ? /step'_incl ?. by apply: rt_trans; [|apply: rt_step]; eassumption. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun