proposition: Lemma simulation' {x y} : reachable M' x y -> valid_state (get_state x) -> valid_state (get_state y) -> reachable M x y.
proof: Proof. Proof using lp_XY Y_fresh XY_neq. by move /reachable_to_reachable_n => [?] /simulation H /H => {}H /H /reachable_n_to_reachable. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun