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