proposition: Theorem flip_consistent_M {s1 t1 X c b1 s2 t2 c2 b2} : In ((s1, t1, X), c, b1) M -> In ((s2, t2, X), c2, b2) M -> b1 = b2.
proof: Proof. move=> /state_flip + /state_flip. case: X; last by congruence. case; (case; by congruence). Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun