proposition: Lemma reachable_0E {X Y} : reachable_n 0 X Y -> X = Y.
proof: Proof. move Hn: (0) => n HXY. case: HXY Hn; first done. by lia. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM