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)))x:A. Dec(P(x)))
Thm*
Thm* ((x:A
B(x)) ~ ((x:A st P(x)B(x))(x:A st 
P(x)B(x)))) (B ~ B') ((AB) ~ (A'B'))| Rank | Theorem | Name |
| 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] |
| cites the following: | ||
| 2 | x:A. Dec(P(x)))
Thm*
Thm* ((x:A B(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x)))) | [card_split_prod_intseg_family_decbl] |
| 1 | (B ~ B') ((AB) ~ (A'B')) | [product_functionality_wrt_one_one_corr] |