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