k:
, P:{P:(k
Prop)| 
i:k. P(i) }.
Thm* (
i:k. Dec(P(i))) 
(
{i:k| P(i) & (j:i. 
P(j)) })x:T. Dec(E(x))) 
(f:(T
). x:T. f(x) E(x))k:, p:{p:(k)| i:k. p(i) }.
Thm* (least i:
. p(i)) {i:k| p(i) & (j:i. p(j)) }| Rank | Theorem | Name |
| 3 | k:, P:{P:(kProp)| i:k. P(i) }.
Thm* ( i:k. Dec(P(i))) ({i:k| P(i) & (j:i. P(j)) }) | [least_exists] |
| cites the following: | ||
| 2 | x:T. Dec(E(x))) (f:(T). x:T. f(x) E(x)) | [dec_pred_iff_some_boolfun] |
| 0 | k:, p:{p:(k)| i:k. p(i) }.
Thm* (least i: . p(i)) {i:k| p(i) & (j:i. p(j)) } | [least_characterized] |