proposition: Lemma uniformly_bounded_empty : mm2_uniformly_bounded [].
proof: Proof. exists 1. move=> x. exists [x]. split; first done. move=> y /clos_rt_rt1n_iff []. - by left. - by move=> ?? [?] [] [[|??]] [?] []. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun