eq:EqDecider(A), P:(A
TypeProp), f,g:x:A fp-> Type.
Thm*
y
dom(f). w=f(y) 
P(y,w)
Thm*
Thm*
ydom(g). w=g(y) P(y,w) ydom(f 
g). w=f g(y) P(y,w)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) fieq:EqDecider(A), f,g:a:A fp-> Top, x:A.
Thm* x
dom(f g) 
x dom(f) 
x dom(g)