Def true == inl()

is mentioned by

Thm* a:Id. a = a ~ true	[eq_id_self]
Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true	[eqof_eq_btrue]

In prior sections: bool 1 sqequal 1 mb list 2 list 1 union mb basic

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