proposition: Lemma mm2_step_sim' x y x' : mm2_step M x y -> sync x x' -> exists y', clos_trans _ (mm2_step M') x' y' /\ sync y y'.
proof: Proof. move=> /mm2_step_sim Hxy. rewrite /sync => <-. exists (shift_state y). by split; [apply: t_step|]. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun