Nuprl Basics - Proof: sfa doc void via isect 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc void via isect 1 1 1 1

1. X :

A:Type. A
2. X

(

A:Type. A)
3. X

{0:

}
4. X

{1:

}
5. X

6. X = 0
7. X

8. X = 1

Void

By:	{Contradiction by X = 0 and X = 1 } Auto

Generated subgoals:

None

About:

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