proposition: Lemma length_preservation : length_preserving M' <-> length_preserving M.
proof: Proof. rewrite /M' /M. constructor; apply: length_preserving_incl; move=> ?; rewrite ?in_app_iff /=; by firstorder done. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun