IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hsum axiom 2
'c,'b,'a:S.
all
(
f:'a 
'c. all
(f:'a 'c. (g:'b 'c. exists_unique
(f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. and
(f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. (all
(f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ((x:'a. equal
(f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ((x:'a. (h(inl(x))
(f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ((x:'a. ,f(x)))
(f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ,all
(f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ,(x:'b. equal
(f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ,(x:'b. (h(inr(x))
(f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ,(x:'b. ,g(x)))))))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
