(6steps total) Remark Remark PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: RussellsParadox Frege 1 1

1. A : Type
2. Q : AAProp
3. P:(AProp). p:Ax:AQ(x,p P(x)
4. p:Ax:AQ(x,p Q(x,x)
  False


By: Analyze4


Generated subgoal:

1 4. p : A
5. x:AQ(x,p Q(x,x)
  False

3 steps

About:
applyfunctionuniversepropfalseallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(6steps total) Remark Remark PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc