IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hlet def11 1. 'b : S
2. 'a : S
(f:'a'b. e:'a. let x = e in f(x)) = (f:'a'b. x:'a. f(x))
By:
Unab [`let`] THEN Simp THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(
f:'a
'b. 
