IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ext simp 11 1. 'a : Type
2. 'b : Type
3. f : 'a'b 4. g : 'a'b 5. (x:'a. f(x)) = (x:'a. g(x))
6. x : 'a f(x) = g(x)
By:
ApplyFunToHypEquands (f:'a'b. f(x)) 5 THEN All Reduce 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)) = (
f(x) = g(x)
