proposition: Lemma Exists_sig {X : Type} P (HP : (forall x, {P x} + {~ P x})) (L : list X) : Exists P L -> { x | In x L /\ P x}.
proof: Proof. elim: L. { by move=> /Exists_nil. } move=> x L IH /Exists_cons H. have [/IH|?] := Exists_dec P L HP. - move=> [y [? ?]]. exists y. by split; [right|]. - exists x. by split; [left|tauto]. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun