IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mul via intseg factors4 1. a,b:, e,g:({a..b}).
1. (x,y. xy)((i:{a..b}. e(i)),i:{a..b}. g(i))
1. =
1. (i:{a..b}. (x,y. xy)(e(i),g(i)))
a,b:, f,g:({a..b}).
(i:{a..b}. f(i))(i:{a..b}. g(i)) = (i:{a..b}. f(i)g(i))
By:
Reduce Hyp:-1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html