| Rank | Theorem | Name |
| 3 | Thm* ( x:A. Dec(P(x)))   (A ~ ({x:A| P(x) }+{x:A|  P(x) })) | [card_split_decbl] |
| cites the following: |
| 0 | Thm* Dec(P)  ( !i: 2. if i= 0 P else P fi) | [decidable_vs_unique_nsub2] |
| 1 | Thm* (A+B) ~ (i:2 if i=0 A else B fi) | [card_union_vs_sigma] |
| 2 | Thm* P:(A  BProp). (x:A. !y:B. P(x;y)) (A ~ (y:B{x:A| P(x;y) })) | [partition_type] |
| 2 | Thm* B,B':(AType). (x:A. B(x) ~ B'(x)) ((x:AB(x)) ~ (x:AB'(x))) | [product_functionality_wrt_one_one_corr_B] |
| 1 | Thm* {x:A| if b P(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi | [ifthenelse_distr_subtype_ooc] |