is mentioned by

Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true	[eqof_eq_btrue]
Thm* d:EqDecider(T), x,y:T. x = y  eqof(d)(x,y)	[deq_property]
Def e = e' == eqof(1of(2of(es)))(e,e')	[es-eq-E]
Def a = b == eqof(KindDeq)(a,b)	[eq_knd]
Def a = b == eqof(IdLnkDeq)(a,b)	[eq_lnk]
Def a = b == eqof(IdDeq)(a,b)	[eq_id]
Def deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x)  b;false;L)	[deq-member]

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