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