proposition: Lemma path_plus {k k' x} y : steps k x = Some y -> path (k+k') x = path k x ++ path k' y.
proof: Proof. move=> Hxy. rewrite /path seq_app map_app /=. congr app. have ->: seq k k' = map (fun i => k+i) (seq 0 k'). { elim: k'; first done. move=> k' IH. have ->: S k' = k' + 1 by lia. by rewrite ?seq_app IH map_app. } rewrite map_map. apply: map_ext => - ?. by rewrite steps_plus' Hxy. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun