proposition: Lemma inverse_simulation {x y} : reachable M x y -> reachable M' x y.
proof: Proof. apply: reachable_incl. by right. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun