proposition: Lemma step_app {M1 M2 x y} : step (M1 ++ M2) x y -> step M1 x y \/ step M2 x y.
proof: Proof. case=> >. rewrite in_app_iff. case=> /transition ?; [by left | by right]. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun