proposition: Lemma reachable_SnE {n X Z} : reachable_n (1+n) X Z -> X = Z \/ (exists Y, reachable_n n X Y /\ step M Y Z).
proof: Proof. move Hn': (1+n) => n' HXY. case: HXY Hn'. - move=> *. by left. - move=> {}n' *. right. have ->: n = n' by lia. by firstorder done. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM