!
{p:(
)| 
x:. p(x) 
prime(x) }P:(AType). (x:A. Dec(P(x))) 
(!{p:(A)| x:A. p(x) P(x) })x:. Dec(prime(x))| Rank | Theorem | Name |
| 12 | !{p:()| x:. p(x) prime(x) } | [prime_decider_exists] |
| cites the following: | ||
| 3 | P:(AType). (x:A. Dec(P(x))) (!{p:(A)| x:A. p(x) P(x) }) | [dec_pred_imp_bool_decider_exists] |
| 11 | x:. Dec(prime(x)) | [decidable__prime] |