proposition: Lemma reachable_n_monotone {X Y m n} : m <= n -> reachable_n m X Y -> reachable_n n X Y.
proof: Proof. elim: n m X Y. { move=> m > ?. have ->: m = 0 by lia. move /reachable_0E => ->. by apply: rn_refl. } move=> n IH [|m] > ?. { move /reachable_0E => ->. by apply: rn_refl. } move /reachable_SnE. case. - move=> ->. by apply: rn_refl. - move=> [Z [? ?]]. apply: rn_step; last by eassumption. apply: IH; last by eassumption. by lia. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM