Def pq == p  q

is mentioned by

Thm* 'a,'b:S. Thm* (p:'a'b. a:'a. b:'b. (a = 1of(p))(b = 2of(p))) Thm* = Thm* (@rep:'a'b'a'b Thm* (@((p',p'':'a'b.  ((rep(p')) = (rep(p'')))(p' = p'')) Thm* (@(x:'a'b Thm* (@(((his_pair('a; 'b)(x)) = (p':'a'b. (x = (rep(p'))))))))

[rep_prod_axiom]

In prior sections: bool 1

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