proposition: Lemma reachable_to_reachable_n {M X Y} : reachable M X Y -> exists n, reachable_n M n X Y.
proof: Proof. move /rt_rt1n. elim; first by (move=> ?; exists 0; apply: rn_refl). move=> > ? _ [n ?]. exists (1+n). apply: rn_step; by eassumption. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun