proposition: Lemma Exists_or_inv : forall (P Q : A -> Prop) l, Exists (fun x => P x \/ Q x) l -> Exists P l \/ Exists Q l.
proof: Proof. intros P Q l; induction l as [|a l IHl]; intro Hl; inversion Hl as [ ? ? H | ? ? H ]; subst. - inversion H; now repeat constructor. - destruct (IHl H); now repeat constructor. Qed.
imports: PeanoNat