Def x : v == <[x],x.v>

is mentioned by

Thm* ltg:(IdLnkIdType), i:Id, k:Knd, T:Type. Thm* (ltg  da-outlinks(k : T;i)) Thm*  Thm* isrcv(k) & source(lnk(k)) = i Thm* & (1of(ltg) ~ lnk(k)) Thm* & (1of(2of(ltg)) ~ tag(k)) Thm* & 2of(2of(ltg)) = T	[da-outlinks-single]
Thm* B:(AType), x:A, v:B(x), eqa:EqDecider(A). x : v  x : v	[fpf-single-sub-reflexive]
Thm* eq:EqDecider(A), B:(AType), x,y:A, v:B(x), u:B(y). Thm* (x = y  v = u  B(x))  x : v || y : u	[fpf-compatible-singles]

In prior sections: mb event system 4

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