IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
inj from empty unique13 1. A : Type
2. B : Type
3. (A)
4. (x.x) AB 5. Inj(A; B; x.x)
(x.x) A injB
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(
A)
x.x) 
B
(
B
