proposition: Lemma monExistsL : forall (A : Type) (P : Pred A) (xs bs cs : list A), ExistsL A P (xs ++ bs) -> ExistsL A P (xs ++ cs ++ bs).
proof: Proof. intros A P xs; elim xs; simpl in |- *; auto. intros a l H' bs cs H'0; inversion H'0; auto. Qed.
imports: Coq(List)