k
) ~ 
k:. (k) ~ B,B':(AType). (x:A. B(x) ~ B'(x)) 
((x:AB(x)) ~ (x:AB'(x))) ~ ) ~ | Rank | Theorem | Name |
| 6 | k) ~ | [card_nat_vs_nat_tuples] |
| cites the following: | ||
| 5 | k:. (k) ~ | [card_nat_vs_nat_tuple] |
| 2 | B,B':(AType). (x:A. B(x) ~ B'(x)) ((x:AB(x)) ~ (x:AB'(x))) | [product_functionality_wrt_one_one_corr_B] |
| 0 | ~ | [nat_plus_ooc_nat] |
| 4 | ) ~ | [card_nat_vs_nat_nat] |