Def proddeq(a;b)(p,q) == (1of(a)(1of(p),1of(q)))(1of(b)(2of(p),2of(q)))

is mentioned

In prior sections: mb event system 2

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