proposition: Lemma step_neq {l r x l' r' y} : X <> x \/ Y <> y -> step M' (l, r, x) (l', r', y) -> step M (l, r, x) (l', r', y).
proof: Proof. move Hx': (l, r, x) => x'. move Hy': (l', r', y) => y' H Hx'y'. case: Hx'y' Hx' Hy' H => > /= []. - move=> ? ? ? [?|?]; by congruence. - move /transition => + ? ? ?. by apply. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun