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

is mentioned by

Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). Thm* prod-deq(A;B;a;b)  (p,q:(AB). p = q  proddeq(a;b)(p,q))	[prod-deq_wf]
Thm* a:EqDecider(A), b:EqDecider(B), p,q:(AB). p = q  proddeq(a;b)(p,q)	[proddeq-property]
Def product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)>	[product-deq]

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