proposition: Lemma reachable_n_to_reachable {M n X Y} : reachable_n M n X Y -> reachable M X Y.
proof: Proof. elim; first by (move=> *; apply: rt_refl). move=> *. apply: rt_trans; last by eassumption. by apply: rt_step. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun