Def  == {i:| 0i }

is mentioned by

Thm* a,b:. a = b  a=b	[nat-deq-aux]
Def SWellFounded(R(x;y)) == f:(T). x,y:T. R(x;y)  f(x)<f(y)	[strongwellfounded]
Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))	[idlnk-deq]
Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)	[id-deq]

In prior sections: int 1 bool 1 int 2 list 1 sqequal 1 mb nat mb list 1 num thy 1 mb list 2 mb event system 1

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