(forall (x) (and (P x) (Q y)))