proposition: Lemma path_S {k x} y : steps 1 x = Some y -> path (S k) x = (Some x) :: (path k y).
proof: Proof. move=> Hxy. rewrite /path /= -seq_shift map_map. congr cons. apply: map_ext => - ? /=. move: Hxy => /=. case: (mm2_sig_step_dec M x) => [[?]|]; last done. by move=> _ [->]. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun