Def f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x)  B(x)

is mentioned by

Thm* eq:EqDecider(T), f,g,h:x:T fp-> Type. Thm* f || g Thm*  Thm* h || f Thm*  Thm* h || g Thm*  Thm* g  h  f  g & f  h  f  g & h  g  h  f  g & h  f  h  f  g	[fpf-compatible-triple]
Thm* eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). Thm* f || h  g || h  f  g || h	[fpf-compatible-join2]
Thm* eq:EqDecider(A), B:(AType), f,g:a:A fp-> B(a). f || g  g || f	[fpf-compatible-symmetry]
Thm* eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). Thm* h || f  h || g  h || f  g	[fpf-compatible-join]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f || g  g  f  g	[fpf-sub-join-right]
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