proposition: Lemma Exists_or : forall (P Q : A -> Prop) l, Exists P l \/ Exists Q l -> Exists (fun x => P x \/ Q x) l.
proof: Proof. intros P Q l; induction l as [|a l IHl]; intros [H | H]; inversion H; subst. 1,3: apply Exists_cons_hd; auto. all: apply Exists_cons_tl, IHl; auto. Qed.
imports: PeanoNat