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