P:(A
Type). (x:A. Dec(P(x))) 
(
!
{p:(A
)| x:A. p(x) 
P(x) })x:T. Dec(E(x))) (f:(T). x:T. f(x) E(x))a,b:. (a b) a = b| Rank | Theorem | Name |
| 3 | P:(AType). (x:A. Dec(P(x))) (!{p:(A)| x:A. p(x) P(x) }) | [dec_pred_imp_bool_decider_exists] |
| cites the following: | ||
| 2 | x:T. Dec(E(x))) (f:(T). x:T. f(x) E(x)) | [dec_pred_iff_some_boolfun] |
| 0 | a,b:. (a b) a = b | [iff_imp_equal_bool] |