proposition: Lemma reaches_steps {x y} : reaches x y -> exists k, steps k x = Some y.
proof: Proof. move=> /clos_rt_rt1n_iff. elim. - move=> >. by exists 0. - move=> {}x {}y z Hxy _ [k Hk]. exists (S k) => /=. case: (mm2_sig_step_dec M x) => [[y' Hxy']|]. + by move: Hxy Hxy' => /mm2_step_det /[apply] <-. + move=> H. by move: Hxy => /H. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun