0+A) ~ A
(B ~ B') ((A+B) ~ (A'+B'))
x:A. Dec(P(x))) (A ~ ({x:A| P(x) }+{x:A| 
P(x) }))| Rank | Theorem | Name |
| 4 | 0+A) ~ A | [card_nsub0_union] |
| cites the following: | ||
| 0 | (B ~ B') ((A+B) ~ (A'+B')) | [union_functionality_wrt_one_one_corr] |
| 3 | x:A. Dec(P(x))) (A ~ ({x:A| P(x) }+{x:A| P(x) })) | [card_split_decbl] |