proposition: Lemma Exists_filter_same : forall P l, Exists P l -> Exists P (filter P l).
proof: Proof. Proof using. introv M. applys* Exists_filter_pred_incl. applys pred_incl_refl. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)