proposition: Lemma bounded_M NM' : bounded M' NM' -> bounded M NM'.
proof: Proof. move=> bounded_M' x. have [L [HL ?]] := bounded_M' x. exists L. constructor; last done. by move=> ? /inverse_simulation /HL. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun