Def  == Unit+Unit

is mentioned by

Thm* B:(AType), eq1,eq2:EqDecider(A), f:a:A fp-> B(a), x:A. Thm* x  dom(f) = x  dom(f)	[fpf-dom_functionality]
Thm* the_w:World, l:IdLnk, t,t':. match(l;t;t')	[w-match_wf]
Thm* the_w:World, e:E. first(e)	[w-first_wf]
Thm* the_w:World, i:Id, t:. first(<i,t>)	[w-first-aux]
Thm* the_w:World, l:IdLnk, i:Id, a:Action(i). isrcv(l;a)	[w-isrcvl_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)	[w-isnull_wf]
Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e')	[es-ble_wf]

In prior sections: bool 1 list 1 rel 1 sqequal 1 mb nat mb list 1 mb list 2 mb event system 1 mb event system 2

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