claim !P:prop.(P -> P) & (P -> P)