A:Type. 
Finite(A) 
Unbounded(A)) (D:Type. (
D) (D))k:
. Infinite(k) Infinite(A) Infinite(B)| Rank | Theorem | Name |
| 7 | A:Type. Finite(A) Unbounded(A)) (D:Type. (D) (D)) | [absurd_nonfin_imp_unb_inf] |
| cites the following: | ||
| 6 | k:. Infinite(k) | [nsub_not_infinite] |
| 0 | Infinite(A) Infinite(B) | [ooc_preserves_infiniteness] |