proposition: Lemma inverse_simulation {n x y} : reachable_n M n x y -> reachable_n M' n x y.
proof: Proof. move=> ?. apply: reachable_n_incl; last by eassumption. by apply: incl_appr. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun