proposition: Lemma Forall_filter_pred_incl : forall P Q l, pred_incl P Q -> Forall Q (filter P l).
proof: Proof. Proof using. introv E. applys~ Forall_pred_incl P. applys Forall_filter_same. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)