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

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* 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:EqDecider(A), x:A, v,z:Top. x : v(x)?z ~ v	[fpf-cap-single1]
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]

In prior sections: mb event system 2 mb event system 3

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