proposition: Lemma reachable_n_monotone {M X Y m n} : m <= n -> reachable_n M m X Y -> reachable_n M 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 => [-> | [Z [? ?]]]; first by apply: rn_refl. apply: rn_step; first by eassumption. apply: IH; last by eassumption. by lia. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun