claim !P:prop.!Q:prop.~ (P | Q) -> ~ P & ~ Q