proposition: Lemma step_fresh_lI l r l' r' x: reachable M (l, r, x) (L ++ l', R ++ r', X) -> reachable M' (l, r, x) (L' ++ l', R' ++ r', Y) .
proof: Proof. Proof using lp_XY. move=> ?. apply: rt_trans. - 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