IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc sexpr car wf1 1. A : Type
2. s : Sexpr(A)
(Case of s : Inj(x) Inj(x) ; Cons(s1;s2) s1) Sexpr(A)
By:
Auto Using:[C(x):= Sexpr(A)]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(Case of s : Inj(x) 
Inj(x) ; Cons(s1;s2) 
Sexpr(A)
