IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ext simp 121 1. 'a : Type
2. 'b : Type
3. f : 'a'b 4. g : 'a'b 5. x:'a. f(x) = g(x)
6. x : 'a f(x) = g(x)
By:
BackThru 5 THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'b
x:'a. f(x) = g(x)
f(x) = g(x)
