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