Nuprl - hol_combin LEMMAs for o

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Theorem	Name
Thm* 'a,'c,'d,'b:S, x:('c 'd), x@0:('b 'c), x@1:('a 'b). Thm* x o (x@0 o x@1) = (x o x@0) o x@1 ('a 'd)	[o_assoc]
cites the following:
Thm* 'a,'c,'d,'b:S. Thm* all Thm* (f:'c 'd. all Thm* (f:'c 'd. (g:'b 'c. all Thm* (f:'c 'd. (g:'b 'c. (h:'a 'b. equal(o(f,o(g,h)),o(o(f,g),h)))))	[ho_assoc]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html