P:{P:(
Prop)| 
i:. P(i) }.
Thm* (
i:. Dec(P(i))) 
(
{i:| P(i) & (j:. j<i 
P(j)) })x:T. Dec(E(x))) 
(f:(T
). x:T. f(x) E(x))p:{p:()| i:. p(i) }.
Thm* (least i:
. p(i)) {i:| p(i) & (j:. j<i p(j)) }| Rank | Theorem | Name |
| 3 | P:{P:(Prop)| i:. P(i) }.
Thm* ( i:. Dec(P(i))) ({i:| P(i) & (j:. j<i P(j)) }) | [least_exists2] |
| cites the following: | ||
| 2 | x:T. Dec(E(x))) (f:(T). x:T. f(x) E(x)) | [dec_pred_iff_some_boolfun] |
| 1 | p:{p:()| i:. p(i) }.
Thm* (least i: . p(i)) {i:| p(i) & (j:. j<i p(j)) } | [least_characterized2] |