proposition: Lemma prod_nat_nat_eq_dec (x y : nat * nat) : {x = y} + {x <> y}.
proof: Proof. by do ? decide equality. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun