fact: Definition M' : SMN := [((L, R, X), (L', R', Y))] ++ M1 ++ M2.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun