proposition: Lemma eq_or_inf {X: Type} : (forall (x y: X), {x = y} + {x <> y}) -> forall (x y: X) P, (x = y) \/ P -> (x = y) + P.
proof: Proof. move=> H x y P. case: (H x y). - move=> ??. by left. - move=> ??. right. tauto. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun