proposition: Lemma unique_step_M'l' {l' r' y} : step M' y (l', r', X) -> l' = [A] ++ skipn 1 l'.
proof: Proof. Proof using unique_step_l' unique_step_l derivable XY_neq. move Hx: (l', r', X) => x Hyx. case: Hyx Hx. move=> v w >. rewrite /M' in_app_iff. case; first by (case; [by congruence | done]). move /transition => /(_ v w) + [] *. subst. by move /unique_step_l'. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun