IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-empty wf1 1. A : Type
2. B : AType
3. x : {x:A| (x nil) }
4. = 5. zzz : Unit
zzzB(x)
By:
Analyze -3 THEN ObviousFrom [-3]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
nil) }
= 
zzz 
