Def o == f:'a'b. g:'a'b. f o g

is mentioned by

Thm* 'c,'b,'a:S. Thm* all Thm* (f:'a  'c. all Thm* (f:'a  'c. (g:'b  'c. exists_unique Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. and Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. (equal(o(h,inl),f) Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,equal(o(h,inr),g)))))

[hsum_axiom]

In prior sections: hol combin

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html