Nuprl - Proof: RussellsParadox Frege 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: RussellsParadox Frege 1 1 1 1

1. A : Type
2. Q : A

Prop
3.

P:(A

Prop).

p:A.

x:A. Q(x,p)

P(x)
4. p : A
5. Q(p,p)

Q(p,p)

False

By:	Thm* (P P) Asserted

Generated subgoal:

1 6. P:Prop. (P P)
False
1 step

About:

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