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

is mentioned by

Thm* eq:EqDecider(A), P:(ATypeProp), x:A, v:Type. Thm* ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)	[fpf-all-single-decl]
Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v) ~ (eqof(eq)(y,x))	[fpf-single-dom-sq]
Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v)  x = y	[fpf-single-dom]
Thm* eq:EqDecider(A), x:A, v,P:Top. z != x : v(x) ==> P(a,z) ~ (True  P(x,v))	[fpf-val-single1]
Thm* eq:EqDecider(A), x,y:A, v,z:Top. Thm* x : v(y)?z ~ if eqof(eq)(x,y) v else z fi	[fpf-cap-single]
Thm* eq,x,v:Top. x : v(x) ~ v	[fpf-ap-single]
Thm* eq:EqDecider(A), x:A, v,z:Top. x : v(x)?z ~ v	[fpf-cap-single1]
Def ma-single-pre-init1(x;T;c;a;T';y,v.P(y;v)) Def == (with ds: x : T Def == (init: x : c Def == action a:T' Def == aprecondition a(v) is Def == as,v. P(s(x);v))	[ma-single-pre-init1]
Def (with ds: ds Def (init: init Def action a:T Def aprecondition a(v) is Def aP) Def == mk-ma(ds; locl(a) : T; init; a : P; ; ; ; )	[ma-single-pre-init]
Def ma-single-pre1(x;A;a;T;y,v.P(y;v)) Def == (with ds: x : A Def == (action a:T Def == (precondition a(v) is Def == (s,v. P(s(x);v) s v)	[ma-single-pre1]
Def (with ds: ds Def (action a:T Def (precondition a(v) is Def (P s v) Def == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; )	[ma-single-pre]
Def ma-single-sends1(A; B; T; x; a; l; tg; f) Def == ma-single-sends(x : A; Def == ma-single-sends(a : B  rcv(l; tg) : T; Def == ma-single-sends(a; Def == ma-single-sends(l; Def == ma-single-sends([<tg,s,v. f(s(x),v)>])	[ma-single-sends1]
Def ma-single-sends(ds; da; k; l; f) == mk-ma(ds; da; ; ; ; <k,l> : f; ; )	[ma-single-sends]
Def ma-single-effect1(x;A;y;B;k;T;f) Def == ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v)))	[ma-single-effect1]
Def ma-single-effect0(x;A;k;T;f) Def == ma-single-effect(x : A; k : T; k; x; (s,v. f(s(x),v)))	[ma-single-effect0]
Def ma-single-effect(ds; da; k; x; f) == mk-ma(ds; da; ; ; <k,x> : f; ; ; )	[ma-single-effect]
Def only L sends on (l with tg) == mk-ma(; ; ; ; ; ; ; <l,tg> : L)	[ma-single-sframe]
Def only members of L affect x :t == mk-ma(x : t; ; ; ; ; ; x : L; )	[ma-single-frame]
Def x : t initially x = v == mk-ma(x : t; ; x : v; ; ; ; ; )	[ma-single-init]

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