M1,M2:MsgA. M1 = M2 
M1 
M2B:(A
Type), eq:EqDecider(A), f,g:a:A fp-> B(a). f = g f g| Theorem | Name |
| M1,M2:MsgA. M1 = M2 M1 M2 | [ma-sub_weakening] |
| cites the following: | |
| B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f = g f g | [fpf-sub_weakening] |