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