x:T. Dec(E(x))) 
(
f:(T
). x:T. f(x) E(x)) (b:. b P)a,b:. (a b) 
a = b| Rank | Theorem | Name |
| 2 | x:T. Dec(E(x))) (f:(T). x:T. f(x) E(x)) | [dec_pred_iff_some_boolfun] |
| cites the following: | ||
| 1 | (b:. b P) | [decbl_iff_some_bool] |
| 0 | a,b:. (a b) a = b | [iff_imp_equal_bool] |