proposition: Lemma Exists_dec l: (forall x:A, {P x} + { ~ P x }) -> {Exists l} + {~ Exists l}.
proof: Proof. intro Pdec. induction l as [|a l' Hrec]. - right. abstract now rewrite Exists_nil. - destruct Hrec as [Hl'|Hl']. + left. now apply Exists_cons_tl. + destruct (Pdec a) as [Ha|Ha]. * left. now apply Exists_cons_hd. * right. abstract now inversion 1. Defined.
imports: PeanoNat