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