proposition: Lemma mm2_step_det {P x y z} : mm2_step P x y -> mm2_step P x z -> y = z.
proof: Proof. by move=> [?] [/mm2_instr_at_unique H /mm2_atom_det H'] [?] [/H <- /H']. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun