A,B:Type, P:(A
BProp).
Thm* (
x:A. 
!y:B. P(x,y)) 
(!f:(AB). x:A. P(x,f(x)))x:A. !y:B. P(x,y)) (f:(AB). x:A. P(x,f(x)))| Rank | Theorem | Name |
| 3 | A,B:Type, P:(ABProp).
Thm* ( x:A. !y:B. P(x,y)) (!f:(AB). x:A. P(x,f(x))) | [unique_indep_fun_description] |
| cites the following: | ||
| 2 | x:A. !y:B. P(x,y)) (f:(AB). x:A. P(x,f(x))) | [indep_fun_description] |