a,a':
. a'-a = 1 
(B:({a..a'
}
Type). (i:{a..a'}
B(i)) ~ B(a))a,a':.
Thm* a'-a = 1
(B:({a..a'}Type). (i:{a..a'}B(i)) ~ ({a:}B(a)))B:({a:A}Type). (i:{a:A}B(i)) ~ B(a)| Rank | Theorem | Name |
| 3 | a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a)) | [card_sum_family_intseg_singleton_elim] |
| cites the following: | ||
| 2 | a,a':.
Thm* a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ ({a:}B(a))) | [card_sum_family_singleton_vs_intseg] |
| 0 | B:({a:A}Type). (i:{a:A}B(i)) ~ B(a) | [card_sum_family_singleton_elim] |