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