Def snd == p:'a'b. 2of(p)

is mentioned by

Thm* 'a,'b:S. all(x:'a. all(y:'b. equal(snd(pair(x,y)),y)))	[hsnd_pair]
Thm* 'a,'b:S. all(x:hprod('a; 'b). equal(pair(fst(x),snd(x)),x))	[hpair_wd]
Thm* 'a,'b:S. Thm* all Thm* (p:hprod('a; 'b). equal Thm* (p:hprod('a; 'b). (snd(p) Thm* (p:hprod('a; 'b). ,select Thm* (p:hprod('a; 'b). ,(y:'b. exists Thm* (p:hprod('a; 'b). ,(y:'b. (x:'a. equal(mk_pair(x,y),rep_prod(p))))))	[hsnd_def]

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