proposition: Lemma mm2_atom_det {mm2i x y z} : mm2_atom mm2i x y -> mm2_atom mm2i x z -> y = z.
proof: Proof. move=> [] > H; inversion H; by subst. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun