IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc sexpr cases wf3 1. A : Type
2. rec(T.(TT)+A)Type
3. rec(T.(TT)+A)
4. s1 : rec(T.(TT)+A)
5. s2 : rec(T.(TT)+A)
inl(<s1,s2>) rec(T.(TT)+A)
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T)+A)
Type
inl(<s1,s2>) 
rec(T.(T
