proposition: Lemma lambda_and_r: forall T (P Q: T -> Prop), (forall a, P a /\ Q a) -> forall a, Q a.
proof: Proof. intros. destruct (H a). trivial. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)