x,y:Id, k:Knd, A,B,T:Type, f:(A
BTA).
Thm*
y = x 
ma-single-effect1(x;A;y;B;k;T;f) 
MsgAeq: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), x,y:A, v:Top. x dom(y : v) 
x = y| Rank | Theorem | Name |
| 5 | x,y:Id, k:Knd, A,B,T:Type, f:(ABTA).
Thm* y = x ma-single-effect1(x;A;y;B;k;T;f) MsgA | [ma-single-effect1_wf] |
| cites the following: | ||
| 4 | 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 fi | [fpf-join-cap-sq] |
| 0 | eq:EqDecider(A), x,y:A, v:Top. x dom(y : v) x = y | [fpf-single-dom] |