proposition: Lemma step_fresh_rI l r l' r' y: reachable M (L ++ l, R ++ r, X) (l', r', y) -> reachable M' (L' ++ l, R' ++ r, Y) (l', r', y).
proof: Proof. Proof using lp_XY. move=> ?. apply: rt_trans; first last. - apply: reachable_incl; last by eassumption. move=> ? ?. by firstorder done. - apply: rt_step. apply: transition. 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