B,B':(A
Type). (x:A. B(x) ~ B'(x)) 
((x:AB(x)) ~ (x:AB'(x)))x:A. B(x) ~ B'(x)) (x:A. B(x)) ~ (x:A. B'(x)) ((x:AB(x)) ~ (x:A'B'(x)))| Rank | Theorem | Name |
| 2 | B,B':(AType). (x:A. B(x) ~ B'(x)) ((x:AB(x)) ~ (x:AB'(x))) | [function_functionality_wrt_one_one_corr_B] |
| cites the following: | ||
| 1 | x:A. B(x) ~ B'(x)) (x:A. B(x)) ~ (x:A. B'(x)) | [one_one_corr_fams_if_one_one_corr_B] |
| 0 | ((x:AB(x)) ~ (x:A'B'(x))) | [card_pi] |