proposition: Lemma length_preserving_M' : length_preserving M'.
proof: Proof. Proof using unique_step_l' unique_step_l derivable XY_neq non_nil length_preserving_M. move=> >. rewrite /M' in_app_iff. case; last by move /length_preserving_M. case; last done. move=> [] *. subst. move=> /=. constructor; last done. have /length_preservingP := derivable. move /(_ length_preserving_M). case; first by congruence. rewrite ?app_length /=. by lia. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun