proposition: Lemma step_fresh_r {l r x} : step M' x (l, r, Y) -> x = (L ++ skipn (length L') l, R ++ skipn (length R') r, X).
proof: Proof. Proof using lp_XY Y_fresh XY_neq. move Hy: (l, r, Y) => y Hyx. case: Hyx Hy => > + [] *. subst. rewrite /M' in_app_iff. move=> [[|[|]]|]. - move=> [] *. subst. by rewrite ?skipn_app ?Nat.sub_diag ?skipn_all. - move=> [] *. by congruence. - done. - have := Y_fresh. rewrite Forall_forall. by move=> H /H []. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun