M:MsgA. ma-is-empty(M) 
M = 
MsgAB:(A
Type), f:x:A fp-> B(x). fpf-is-empty(f) f = x:A fp-> B(x)| Rank | Theorem | Name |
| 2 | M:MsgA. ma-is-empty(M) M = MsgA | [assert-ma-is-empty] |
| cites the following: | ||
| 1 | B:(AType), f:x:A fp-> B(x). fpf-is-empty(f) f = x:A fp-> B(x) | [assert-fpf-is-empty] |