Def fst == p:'a'b. 1of(p)

is mentioned by

Thm* 'a,'b:S. all(x:'a. all(y:'b. equal(fst(pair(x,y)),x)))	[hfst_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). (fst(p) Thm* (p:hprod('a; 'b). ,select Thm* (p:hprod('a; 'b). ,(x:'a. exists Thm* (p:hprod('a; 'b). ,(x:'a. (y:'b. equal(mk_pair(x,y),rep_prod(p))))))	[hfst_def]

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