A,B:MsgA.
Thm* A || B
Thm*
Thm* ma-frame-compatible(A; B)
Thm*
Thm* ma-sframe-compatible(A; B)
Feasible(A) Feasible(B) Feasible(A 
B)B:(A
Type), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x
dom(f g) 
x dom(f) 
x dom(g)B:(AType), 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). f || g g 
f gB1,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. g f (x:X. f(x)?Top r g(x)?Top)eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top.
Thm* f
g(x)?z ~ if x dom(f) f(x)?z else g(x)?z fieq: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)