proposition: Lemma fresh_StateP {M: SMN} {l r x l' r' y} : In ((l, r, x), (l', r', y)) M -> x < fresh_State M /\ y < fresh_State M.
proof: Proof. elim: M; first done. move=> [[[l1 r1] x1] [[l2 r2] x2]] M IH /= [|]. - move=> [] *. subst. by lia. - move /IH. by lia. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun