IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc sexpr inj wf A:Type, a:A. Inj(a) Sexpr(A)
By:
Def of Inj(a) | Sexpr(A) THEN Repeat Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
A:Type, a:A. Inj(a) 
Sexpr(A)
