M1,M2:MsgA. M1 || M2 
M2 || M1B:(A
Type), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x
dom(f 
g) f g(x) = if x dom(f)
f(x) else g(x) fi B(x)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)B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a).
Thm* f
f geq:EqDecider(X), f,g:x:X fp-> Type, x:X. g f (f(x)?T r g(x)?Top)ds,ds':ltg:Id fp-> Type. ds ds' State(ds') State(ds)eq:EqDecider(X), f,g:x:X fp-> Type, x:X. f g (f(x)?Void r g(x)?T)