B:(A
Type), P:(x:AB(x)Prop).
Thm* (
x:A. 
!y:B(x). P(x,y)) 
(!
{f:(x:AB(x))| x:A. P(x,f(x)) })B:(AType), P:(x:AB(x)Prop).
Thm* (
x:A. !y:B(x). P(x,y)) (!f:(x:AB(x)). x:A. P(x,f(x)))| Rank | Theorem | Name |
| 3 | B:(AType), P:(x:AB(x)Prop).
Thm* ( x:A. !y:B(x). P(x,y)) (!{f:(x:AB(x))| x:A. P(x,f(x)) }) | [unique_fun_description2] |
| cites the following: | ||
| 2 | B:(AType), P:(x:AB(x)Prop).
Thm* ( x:A. !y:B(x). P(x,y)) (!f:(x:AB(x)). x:A. P(x,f(x))) | [unique_fun_description] |