Def true == inl()

is mentioned by

Thm* b:. b  b = true	[assert_imp_eq_btrue]
Thm* true  True	[assert_of_btrue]
Thm* false = true  False	[btrue_neq_bfalse_simp_2]
Thm* true = false  False	[btrue_neq_bfalse_simp_1]
Def isr(x) == InjCase(x; y. false; z. true)	[isr]
Def P == InjCase(lem_2(P) ; true; false)	[prop_to_bool_2]
Def P == InjCase(lem(P) ; true; false)	[prop_to_bool]

In prior sections: bool 1

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