proposition: Theorem Exists_impl : forall (P Q : A -> Prop), (forall a : A, P a -> Q a) -> forall l, Exists P l -> Exists Q l.
proof: Proof. intros P Q H l H0. induction H0 as [x l H0|x l H0 IHExists]. - apply (Exists_cons_hd Q x l (H x H0)). - apply (Exists_cons_tl x IHExists). Qed.
imports: PeanoNat