a,a':
.
Thm* a'-a = 1
(B:({a..a'
}
Type). (i:{a..a'}
B(i)) ~ ({a:}B(a)))a,a':.
Thm* a'-a = 1
(B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))| Rank | Theorem | Name |
| 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] |
| cites the following: | ||
| 1 | a,a':.
Thm* a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a))) | [exteq_sum_family_singleton_vs_intseg] |