M1,M2:MsgA. M1 || M2 
Prop{i'}B:(A
Type), 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, x:X. f g (f(x)?Void r g(x)?T)eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g f (f(x)?T r g(x)?Top)B1,B2:(AType).
Thm* (
a:A. B1(a) r B2(a)) (a:A fp-> B1(a) r a:A fp-> B2(a))