IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hs def 'c,'b,'a:S. equal(s,f:'a'b'c. g:'a'b. x:'a. f(x,g(x)))
By:
Simpsetp [`hol_to_nuprl`] THEN StrongAuto
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
'c,'b,'a:S. equal(s,
f:'a 
'b 
