proposition: Lemma uniform_decision_0 a b : (terminating (1, (a, b))) + (non_terminating (1, (a, b))).
proof: Proof. Proof using HM. have [v []] := get_representative (a, b). move=> /uniform_representative_decision [] => H /H; tauto. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun