hol pair Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* 'a,'b:S, b:'ba:'ay:'bx:'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
hol pair Sections HOLlib Doc