proposition: Lemma length_preservation : length_preserving M' <-> length_preserving M.
proof: Proof. Proof using non_nil derivable. constructor; first by (apply: length_preserving_incl; right). move=> HM >. rewrite /M' in_app_iff. case; last by move /HM. case; last done. move=> [] *. subst. move: (derivable) => /(length_preservingP HM). case; last done. move=> [] *. by subst. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun