Def a:A fp-> B(a) == d:A Lista:{a:A| (a  d) }B(a)

is mentioned by

Thm* A:Type, eq:EqDecider(A), f:a:A fp-> Top. Thm* fpf-dom-list(f)  {a:A| a  dom(f) } List	[fpf-dom-list_wf]
Thm* eq:EqDecider(A), B:Top, f:a:A fp-> Top.  || f	[fpf-empty-compatible-left]
Thm* eq:EqDecider(A), B:Top, f:a:A fp-> Top. f ||	[fpf-empty-compatible-right]
Thm* A:Type, B:(AType), x:A, v:B(x). x : v  x:A fp-> B(x)	[fpf-single_wf]
Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A. Thm* f  g(x) ~ if x  dom(f) f(x) else g(x) fi	[fpf-join-ap-sq]
Thm* eq:EqDecider(A), f,g:x:A fp-> Top. Thm* fpf-is-empty(f  g) ~ (fpf-is-empty(f)fpf-is-empty(g))	[fpf-join-is-empty]
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A. Thm* x  dom(f  g)  x  dom(f)  x  dom(g)	[fpf-join-dom2]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x  dom(f  g)  x  dom(f)  x  dom(g)	[fpf-join-dom]
Def MsgAForm Def == x:Id fp-> Topx:Knd fp-> Typex:Id fp-> Topx:Id fp-> Top Def == x:KndId fp-> Topx:KndIdLnk fp-> Topx:Id fp-> Topx:IdLnkId fp-> Top Def == Top	[msg-form]
Def MsgA Def == ds:x:Id fp-> Type Def == da:a:Knd fp-> Type Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void Def == kl:KndIdLnk fp-> (tg:Id Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop	[msga]

In prior sections: mb event system 3

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