proposition: Lemma bounded_to_bounded' {n: nat}: bounded M n -> exists (m: nat), bounded' m.
proof: Proof. move=> Hn. exists (n+n). rewrite /bounded'. move=> [[A' B'] z] x y A B /(bounded_stack_difference Hn) + /(bounded_stack_difference Hn) => /=. by lia. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM