a,b:
, c:{a...b}, B:({a..b
}
Type).
Thm* (i:{a..b
}
B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i)))B:(AType), P:(AProp).
Thm* (
i:A. Dec(P(i)))
Thm*
Thm* ((i:A
B(i)) ~ ((i:{i:A| P(i) }B(i))+(i:{i:A| 
P(i) }B(i)))) (B ~ B') ((A+B) ~ (A'+B'))| Rank | Theorem | Name |
| 5 | a,b:, c:{a...b}, B:({a..b}Type).
Thm* (i:{a..b }B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i))) | [card_split_sum_intseg_family] |
| cites the following: | ||
| 4 | B:(AType), P:(AProp).
Thm* ( i:A. Dec(P(i)))
Thm*
Thm* ((i:A B(i)) ~ ((i:{i:A| P(i) }B(i))+(i:{i:A| P(i) }B(i)))) | [card_split_sigma_dom_decbl] |
| 0 | (B ~ B') ((A+B) ~ (A'+B')) | [union_functionality_wrt_one_one_corr] |