proposition: Lemma stepI {M: SMN} {X Y: Config} v w l r l' r' x y : X = (l ++ v, r ++ w, x) -> Y = (l' ++ v, r' ++ w, y) -> In ((l, r, x), (l', r', y)) M -> step M X Y.
proof: Proof. move=> -> -> /transition. by apply. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun