proposition: Theorem boundedP : (exists n, bounded M n) <-> (exists m, bounded' m).
proof: Proof. Proof using confluent_M. constructor. - move=> [?]. by apply /bounded_to_bounded'. - move=> [?]. by apply /bounded_of_bounded'. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM