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