proposition: Lemma mm2_state_eq_dec (x y: mm2_state) : {x = y} + {x <> y}.
proof: Proof. do ? decide equality. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun