Def EqDecider(T) == eq:TTx,y:T. x = y  (eq(x,y))

is mentioned by

Thm* E:Type, eq:EqDecider(E), T,V:(IdIdType), M:(IdLnkIdType), Thm* loc:(EId), k:(EKnd), v:(e:Eeventtype(k;loc;V;M;e)), Thm* w,a:(x:Ide:ET(loc(e),x)), snds:(l:IdLnkE(Msg_sub(l; M) List)), Thm* sndr:({e:E| isrcv(k(e)) }E), i:(e:{e:E| isrcv(k(e)) }||snds Thm* sndr:({e:E| isrcv(k(e)) }E), i:(e:{e:E| isrcv(k(e)) }||(lnk(k(e)) Thm* sndr:({e:E| isrcv(k(e)) }E), i:(e:{e:E| isrcv(k(e)) }||,sndr(e))||), Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms{i:l} Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(E; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(T; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(M; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(loc; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(k; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(v; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(w; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(a; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(snds; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(sndr; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(i; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(f; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(prd; Thm* f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(cl). Thm* mk-es(E; eq; T; V; M; loc; k; v; w; a; snds; sndr; i; f; prd; cl; p)  ES	[mk-es_wf]
Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L)	[assert-deq-member]
Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). Thm* sum-deq(A;B;a;b)  (p,q:A+B. p = q  sumdeq(a;b)(p,q))	[sum-deq_wf]
Thm* a:EqDecider(A), b:EqDecider(B), p,q:A+B. p = q  sumdeq(a;b)(p,q)	[sumdeq-property]
Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). Thm* prod-deq(A;B;a;b)  (p,q:(AB). p = q  proddeq(a;b)(p,q))	[prod-deq_wf]
Thm* a:EqDecider(A), b:EqDecider(B), p,q:(AB). p = q  proddeq(a;b)(p,q)	[proddeq-property]
Thm* strong-subtype(A;B)  (EqDecider(B) r EqDecider(A))	[strong-subtype-deq-subtype]
Thm* d:EqDecider(B). strong-subtype(A;B)  d  EqDecider(A)	[strong-subtype-deq]
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 ES Def == E:Type Def == EqDecider(E)(T:IdIdType Def == EqDecider(E)(V:IdIdType Def == EqDecider(E)(M:IdLnkIdType Def == EqDecider(E)(Top(loc:EId Def == EqDecider(E)(Top(kind:EKnd Def == EqDecider(E)(Top(val:(e:Eeventtype(kind;loc;V;M;e)) Def == EqDecider(E)(Top(when:(x:Ide:ET(loc(e),x)) Def == EqDecider(E)(Top(after:(x:Ide:ET(loc(e),x)) Def == EqDecider(E)(Top(sends:(l:IdLnkE(Msg_sub(l; M) List)) Def == EqDecider(E)(Top(sender:{e:E| isrcv(kind(e)) }E Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||sends Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||(lnk(kind(e)) Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||,sender(e))||) Def == EqDecider(E)(Top(first:E Def == EqDecider(E)(Top(pred:{e':E| (first(e')) }E Def == EqDecider(E)(Top(causl:EEProp Def == EqDecider(E)(Top(ESAxioms{i:l} Def == EqDecider(E)(Top(ESAxioms(E; Def == EqDecider(E)(Top(ESAxioms(T; Def == EqDecider(E)(Top(ESAxioms(M; Def == EqDecider(E)(Top(ESAxioms(loc; Def == EqDecider(E)(Top(ESAxioms(kind; Def == EqDecider(E)(Top(ESAxioms(val; Def == EqDecider(E)(Top(ESAxioms(when; Def == EqDecider(E)(Top(ESAxioms(after; Def == EqDecider(E)(Top(ESAxioms(sends; Def == EqDecider(E)(Top(ESAxioms(sender; Def == EqDecider(E)(Top(ESAxioms(index; Def == EqDecider(E)(Top(ESAxioms(first; Def == EqDecider(E)(Top(ESAxioms(pred; Def == EqDecider(E)(Top(ESAxioms(causl) Def == EqDecider(E)(Top(Top))	[event_system]
Def DS(A) == sort:ATypea:AEqDecider(sort(a))	[discrete_struct]

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