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))))x:A. 
!y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x)))
(!i:
2. if i=
0
P else P fi)| Rank | Theorem | Name |
| 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] |
| cites the following: | ||
| 1 | x:A. !y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x))) | [fun_description] |
| 0 | (!i:2. if i=0 P else P fi) | [decidable_vs_unique_nsub2] |