a,a':
. a'-a = 1 
(B:({a..a'
}
Type). (i:{a..a'}B(i)) ~ B(a))a,a':. a'-a = 1 ({a..a'} =ext {a:})B(i)) ~ B(a)| Rank | Theorem | Name |
| 2 | a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a)) | [card_prod_family_intseg_singleton_elim] |
| cites the following: | ||
| 0 | a,a':. a'-a = 1 ({a..a'} =ext {a:}) | [exteq_singleton_vs_intseg] |
| 1 | B(i)) ~ B(a) | [card_prod_family_singleton_elim] |