proposition: Lemma reachable_incl {M1 M2 X Y} : incl M1 M2 -> reachable M1 X Y -> reachable M2 X Y.
proof: Proof. move=> /reachable_n_incl H /reachable_to_reachable_n [?] ?. apply: reachable_n_to_reachable. apply: H. by eassumption. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun