k:
. (k
) ~ a,b:
, c:{a...b}, B:({a..b
}Type).
Thm* (i:{a..b
}B(i)) ~ ((i:{a..c}B(i))
(i:{c..b}B(i)))a,a':. a'-a = 1 
(B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))) ~ | Rank | Theorem | Name |
| 5 | k:. (k) ~ | [card_nat_vs_nat_tuple] |
| cites the following: | ||
| 3 | a,b:, c:{a...b}, B:({a..b}Type).
Thm* (i:{a..b }B(i)) ~ ((i:{a..c}B(i))(i:{c..b}B(i))) | [card_split_prod_intseg_family] |
| 2 | a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a)) | [card_prod_family_intseg_singleton_elim] |
| 4 | ) ~ | [card_nat_vs_nat_nat] |