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 cons wf A:Type, s1,s2:Sexpr(A). Cons(s1;s2) Sexpr(A)
By:
Def of Sexpr(A) | Cons(s1;s2) 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, s1,s2:Sexpr(A). Cons(s1;s2) 
Sexpr(A)
