proposition: Lemma P_to_M s t : ((1, P) // s ->> t) -> exists n, Nat.iter n (obind (MPM2.step M)) (Some (to_Config s)) = Some (to_Config t).
proof: Proof. move=> [n Hn]. exists n. elim: n s Hn. { by move=> s /sss_steps_0_inv <-. } move=> n IH s /sss_steps_S_inv' [u] [/P_to_M_step Hsu] /IH {}IH. by rewrite /= obind_oiter Hsu. Qed.
imports: PeanoNat Lia List Undecidability.MinskyMachines(MM MM_sss) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) ssreflect ssrbool ssrfun