hol pair Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* 'a,'b:S, x:'ay:'by = y[snd_pair]
cites the following:
Thm* 'a,'b:S. all(x:'a. all(y:'b. equal(snd(pair(x,y)),y)))[hsnd_pair]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol pair Sections HOLlib Doc