Thm*  a,b,c:. a(bc) = (ab)c

This is just an amusing alternative derivation through cardinality of something Auto can already prove. We had to go out of our way to keep Auto from proving it.

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