proposition: Lemma step_incl {M1 M2 X Y} : incl M1 M2 -> step M1 X Y -> step M2 X Y.
proof: Proof. move=> HM1M2. case=> > /HM1M2. by apply: transition. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun