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