IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc sexpr atom wf112 1. A : Type
2. s : rec(T.(TT)+A)
3. Size(s) = 1
4. y : A 5. s = inr(y)
sexprAtom(inr(y)) A
By:
Compute sexprAtom(inr(y)) *y
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T)+A)
sexprAtom(inr(y)) 
A
y
