Def false == inr()

is mentioned by

Thm* 'a:S. (x:'a. false) = false	[ball_bfalse]
Thm* 'a:S. (x:'a. false) = false	[bexists_bfalse]
Thm* p:. false = p  p	[equal_bfalse_to_assert_2]
Thm* p:. p = false  p	[equal_bfalse_to_assert]
Thm* false = true	[bnot_simp_2]
Thm* true = false	[bnot_simp_1]
Thm* b:. (bfalse) = false	[band_simp_2]
Thm* b:. (falseb) = false	[band_simp_4]
Thm* b:. (false  b) = b	[bor_simp_4]
Thm* b:. (b  false) = b	[bor_simp_2]
Def f == false	[hf]

In prior sections: bool 1 hol

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