proposition: Lemma reachable_n_incl {M1 M2 n X Y} : incl M1 M2 -> reachable_n M1 n X Y -> reachable_n M2 n X Y.
proof: Proof. move=> H. elim: n X Y. { move=> > /reachable_0E ->. by apply: rn_refl. } move=> n IH > /reachable_SnE. case. - move=> ->. by apply: rn_refl. - move=> [?] [? ?]. apply: rn_step. + apply: step_incl; by eassumption. + by apply: IH. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun