(3steps total) PrintForm NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc whatever in void dom fun 1
1. A : Type
  (x.whatever) = (x.x)  VoidA
By: FunExtensionality

Generated subgoal:

1 2. x : Void
  whatever = x  A
1 step

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

(3steps total) PrintForm NuprlPrimitives Sections NuprlLIB Doc