proposition: Corollary reaches'_incl {x y} : reaches' x y -> reaches x y.
proof: Proof. by move=> [k /steps'_incl]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun