L:MsgA List. ma-is-empty(
(L)) ~ reduce(
M,x. ma-is-empty(M)
x;true;L)L:MsgA List. (L) 
MsgAForma,b:
. (a 
b) 
a = beq:EqDecider(A), f,g:x:A fp-> Top.
Thm* fpf-is-empty(f
g) ~ (fpf-is-empty(f)fpf-is-empty(g))| Rank | Theorem | Name |
| 5 | L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M)x;true;L) | [ma-join-list-is-empty] |
| cites the following: | ||
| 1 | L:MsgA List. (L) MsgAForm | [msg-form-join-list] |
| 0 | a,b:. (a b) a = b | [iff_imp_equal_bool] |
| 4 | eq:EqDecider(A), f,g:x:A fp-> Top.
Thm* fpf-is-empty(f g) ~ (fpf-is-empty(f)fpf-is-empty(g)) | [fpf-join-is-empty] |