Def b == if b True else False fi

is mentioned by

Thm* 'b,'a:S. all(f:'a  'b. and(equal(o(i,f),f),equal(o(f,i),f)))	[hi_o_id]
Thm* 'a:S. all(x:'a. equal(i(x),x))	[hi_thm]
Thm* 'a,'b,'c:S. Thm* all Thm* (f:'a  'b  'c. all Thm* (f:'a  'b  'c. (g:'a  'b. all(x:'a. equal(s(f,g,x),f(x,g(x))))))	[hs_thm]
Thm* 'a,'b:S. all(x:'a. all(y:'b. equal(k(x,y),x)))	[hk_thm]
Thm* 'a,'c,'d,'b:S. Thm* all Thm* (f:'c  'd. all Thm* (f:'c  'd. (g:'b  'c. all Thm* (f:'c  'd. (g:'b  'c. (h:'a  'b. equal(o(f,o(g,h)),o(o(f,g),h)))))	[ho_assoc]
Thm* 'b,'c,'a:S. Thm* all(f:'b  'c. all(g:'a  'b. all(x:'a. equal(o(f,g,x),f(g(x))))))	[ho_thm]
Thm* 'a:S. equal(i,s(k,k))	[hi_def]
Thm* 'c,'b,'a:S. equal(s,f:'a  'b  'c. g:'a  'b. x:'a. f(x,g(x)))	[hs_def]
Thm* 'a,'b:S. equal(k,x:'a. y:'b. x)	[hk_def]
Thm* 'c,'b,'a:S. Thm* all(f:'b  'c. all(g:'a  'b. equal(o(f,g),x:'a. f(g(x)))))	[ho_def]

In prior sections: bool 1 hol hol bool hol min

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