A:Type. 
Finite(A) 
Unbounded(A)) (P:Prop. P 
P)A:Type. Finite(A) Unbounded(A)) (D:Type. (
D) (D))A:Type. P = (A) PropP:Prop. P P) (A:Type. Finite(A) Unbounded(A)) Finite(A)| Rank | Theorem | Name |
| 8 | A:Type. Finite(A) Unbounded(A)) (P:Prop. P P) | [nonfin_eqv_unb_inf_iff_negnegelim] |
| cites the following: | ||
| 7 | A:Type. Finite(A) Unbounded(A)) (D:Type. (D) (D)) | [absurd_nonfin_imp_unb_inf] |
| 0 | A:Type. P = (A) Prop | [inhab_rep_axiom] |
| 4 | P:Prop. P P) (A:Type. Finite(A) Unbounded(A)) | [negnegelim_imp_notfin_imp_unb_inf] |
| 4 | Finite(A) | [unb_inf_not_fin] |