proposition: Lemma length_preserving_incl {M1 M2} : incl M1 M2 -> length_preserving M2 -> length_preserving M1.
proof: Proof. by move=> H12 H2 > /H12 /H2. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun