P:(('a
'a
)Prop).
Thm* P(<eq_pred:(
x:'a. y:'a. x =
y)>) 
(f:eq('a). P(f))f:eq('a). f = (x:'a. y:'a. x = y) 
'a'a| Theorem | Name |
| P:(('a'a)Prop).
Thm* P(<eq_pred:( x:'a. y:'a. x = y)>) (f:eq('a). P(f)) | [eq_pred_abstraction] |
| cites the following: | |
| f:eq('a). f = (x:'a. y:'a. x = y) 'a'a | [eq_pred_char] |