proposition: Lemma fresh_StateP' (M: SMN) : Forall (fun '((_, _, x), (_, _, y)) => x <> fresh_State M /\ y <> fresh_State M) M.
proof: Proof. rewrite Forall_forall. move=> [[[l1 r1] x1] [[l2 r2] x2]] /fresh_StateP. by lia. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun