fact: Variable unique_step_l' : forall l' r' y, step M y (l', r', X) -> l' = [A] ++ skipn 1 l'.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun