proposition: Lemma simulation_step {x y} : step M' x y <-> step M x y.
proof: Proof. constructor; apply: step_incl=> ?; rewrite /M /M' ?in_app_iff /=; by firstorder done. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun