IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
RussellsParadox Frege11111 1. A : Type
2. Q : AAProp
3. P:(AProp). p:A. x:A. Q(x,p) P(x)
4. p : A 5. Q(p,p) Q(p,p)
6. P:Prop. (PP)
False
By:
Witness6: Q(p,p) { contradicting Hyp:5 }
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html