IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
No proposition is equivalent to its own negation.
At:
no prop iff its neg
P:Prop.
(P ![](FONT/if_big.png)
P)
Generated subgoal:
1 |
1. P : Prop
2. P ![](FONT/if_big.png) P
False
![](FONT/BLANK.png) | 6 steps |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html