A:Type. 
Finite(A) 
Infinite(A)) (D:Type. (
D) (D))A:Type. Finite(A) Unbounded(A)) (D:Type. (D) (D)) Unbounded(A)| Rank | Theorem | Name |
| 8 | A:Type. Finite(A) Infinite(A)) (D:Type. (D) (D)) | [absurd_nonfinite_imp_infinite] |
| cites the following: | ||
| 7 | A:Type. Finite(A) Unbounded(A)) (D:Type. (D) (D)) | [absurd_nonfin_imp_unb_inf] |
| 0 | Unbounded(A) | [unboundedly_imp_productively_infinite] |