k
) ~ 
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))))a,a':
. a'-a = 1 (B:({a..a'
}Type). (i:{a..a'}B(i)) ~ B(a))0A) ~ 1
k) ~ k:. (k+) ~ | Rank | Theorem | Name |
| 7 | k) ~ | [card_nat_vs_nat_tuples_all] |
| 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] |
| 3 | a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a)) | [card_sum_family_intseg_singleton_elim] |
| 1 | 0A) ~ 1 | [card_void_dom_fun_unit] |
| 6 | k) ~ | [card_nat_vs_nat_tuples] |
| 0 | k:. (k+) ~ | [fin_plus_nat_ooc_nat] |