Nuprl - hol_pair LEMMAs for pair

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

Theorem	Name
Thm* 'a,'b:S, b:'b, a:'a, y:'b, x:'a. <x,y> = <a,b> x = a & y = b	[pair_eq]
cites the following:
Thm* 'a,'b:S. Thm* all Thm* (b:'b. all Thm* (b:'b. (a:'a. all Thm* (b:'b. (a:'a. (y:'b. all Thm* (b:'b. (a:'a. (y:'b. (x:'a. equal Thm* (b:'b. (a:'a. (y:'b. (x:'a. (equal(pair(x,y),pair(a,b)) Thm* (b:'b. (a:'a. (y:'b. (x:'a. ,and(equal(x,a),equal(y,b)))))))	[hpair_eq]

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