Def S == {T:Type| x:T. True }

is mentioned by

Thm* 'a,'b:S, p:('a'b). p = <1of(p),2of(p)>	[pair_unfold]
Thm* 'a,'b:S, b:'b, a:'a, y:'b, x:'a. <x,y> = <a,b>  x = a & y = b	[pair_eq]
Thm* 'a,'b:S, x:'a, y:'b. y = y	[snd_pair]
Thm* 'a,'b:S, x:'a, y:'b. x = x	[fst_pair]
Thm* 'a,'b:S, x:('a'b). <1of(x),2of(x)> = x	[pair_wd]
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]
Thm* 'a,'b:S. all(x:'a. all(y:'b. equal(snd(pair(x,y)),y)))	[hsnd_pair]
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* 'c,'a,'b:S. Thm* all Thm* (f:hprod('a; 'b)  'c. all Thm* (f:hprod('a; 'b)  'c. (x:'a. all Thm* (f:hprod('a; 'b)  'c. (x:'a. (y:'b. equal Thm* (f:hprod('a; 'b)  'c. (x:'a. (y:'b. (curry(f,x,y) Thm* (f:hprod('a; 'b)  'c. (x:'a. (y:'b. ,f(pair(x,y))))))	[hcurry_def]
Thm* 'c,'a,'b:S. Thm* all Thm* (f:'a  'b  'c. all Thm* (f:'a  'b  'c. (x:'a. all Thm* (f:'a  'b  'c. (x:'a. (y:'b. equal(uncurry(f,pair(x,y)),f(x,y)))))	[huncurry_def]
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]
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]
Thm* 'a,'b:S. Thm* all Thm* (x:'a. all Thm* (x:'a. (y:'b. equal Thm* (x:'a. (y:'b. (pair(x,y) Thm* (x:'a. (y:'b. ,select Thm* (x:'a. (y:'b. ,(p:hprod('a; 'b). equal(rep_prod(p),mk_pair(x,y))))))	[hcomma_def]
Thm* 'a,'b:S. Thm* exists Thm* (rep:hprod('a; 'b)  'a  'b  hbool. type_definition(is_pair,rep))	[hprod_ty_def]
Thm* 'a,'b:S. Thm* equal Thm* (rep_prod Thm* ,select Thm* ,(rep:hprod('a; 'b) Thm* ,( 'a Thm* ,( 'b Thm* ,( hbool. and Thm* ,( hbool. (all Thm* ,( hbool. ((p':hprod('a; 'b). all Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). implies Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). (equal Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). ((rep(p') Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). (,rep(p'')) Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). ,equal(p',p'')))) Thm* ,( hbool. ,all Thm* ,( hbool. ,(p:'a  'b  hbool. equal Thm* ,( hbool. ,(p:'a  'b  hbool. (is_pair(p) Thm* ,( hbool. ,(p:'a  'b  hbool. ,exists Thm* ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). equal Thm* ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). (p Thm* ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). ,rep(p'))))))))	[hrep_prod_wd]
Thm* 'a,'b:S. Thm* all Thm* (p:'a  'b  hbool. equal Thm* (p:'a  'b  hbool. (is_pair(p) Thm* (p:'a  'b  hbool. ,exists Thm* (p:'a  'b  hbool. ,(x:'a. exists(y:'b. equal(p,mk_pair(x,y))))))	[his_pair_def]
Thm* 'a,'b:S. Thm* all Thm* (x:'a. all Thm* (x:'a. (y:'b. equal Thm* (x:'a. (y:'b. (mk_pair(x,y) Thm* (x:'a. (y:'b. ,a:'a. b:'b. and(equal(a,x),equal(b,y)))))	[hmk_pair_def]
Thm* 'a,'b:S. hprod('a; 'b)  S	[hprod_wf]
Thm* 'a,'b,'c:S. curry  ((hprod('a; 'b)  'c)  'a  'b  'c)	[hcurry_wf]

In prior sections: hol hol min hol bool

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