IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-single-pre-init1 wf2 1. T : Type
2. T' : Type
3. x : Id
4. T 5. Id
6. TT'Prop
(x@0.x : T(x@0)?Void) IdType
By:
AssertBY (Void Type) Auto
THEN
Repeat (Unfolds [`fpf-single`;`fpf-dom`;`fpf-cap`;`fpf-ap`] 0 THEN Reduce 0)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T'
(
x@0.x : T(x@0)?Void) 
Id
