(5steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc void via isect 1 1 1
1. X : A:Type. A
2. X  (A:Type. A)
3. X  {0:}
4. X  {1:}
  X  Void
By: Analyze3 THEN Analyze4

Generated subgoal:

1 5. X  
6. X = 0
7. X  
8. X = 1
  X  Void
1 step

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

(5steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc