P:(A
BProp). (x:A. 
!y:B. P(x;y)) 
(A ~ (y:B
{x:A| P(x;y) }))x:A. !y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x)))| Rank | Theorem | Name |
| 2 | P:(ABProp). (x:A. !y:B. P(x;y)) (A ~ (y:B{x:A| P(x;y) })) | [partition_type] |
| cites the following: | ||
| 1 | x:A. !y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x))) | [fun_description] |