(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 isect2 1 1
1. X : x:. {x:}
2. X  (x:. {x:})
  X  Void
By: Witness2: 0 THEN Witness2: 1

Generated subgoal:

1 3. X  {0:}
4. X  {1:}
  X  Void
2 steps

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

(5steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc