proposition: Lemma subPredExistsL : forall (A B : Type) (P : Pred A) (S : Pred B) (f : A -> B), (forall a : A, P a -> S (f a)) -> forall l : list A, ExistsL A P l -> ExistsL B S (map f l).
proof: Proof. intros A B P S f H' l H'0; elim H'0; simpl in |- *; auto. Qed.
imports: Coq(List)