IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc type poly identity112 1. f : D:Type. DD 2. A : Type
3. a : A 4. f {a:A}{a:A}
a {a:A}
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
D:Type. D
D
{a:A}
a 
