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)))x:A. !y:B(x). P(x,y)) (f:(x:AB(x)). x:A. P(x,f(x)))| Rank | Theorem | Name |
| 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] |
| cites the following: | ||
| 1 | x:A. !y:B(x). P(x,y)) (f:(x:AB(x)). x:A. P(x,f(x))) | [fun_description] |