i,j:
, F:({i..j
}
Prop). (k:{i..j}. Dec(F(k))) 
Dec(k:{i..j}. F(k))i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k))) Dec(
k:{i..j}. F(k)) Dec(
P)Q:(TProp). (x:T. Q(x)) 
(x:T. Q(x)) (A A)| Rank | Theorem | Name |
| 7 | i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k)) | [decidable__all_int_seg] |
| cites the following: | ||
| 6 | i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k)) | [decidable__ex_int_seg] |
| 0 | Dec(P) | [decidable__not] |
| 0 | Q:(TProp). (x:T. Q(x)) (x:T. Q(x)) | [not_over_exists] |
| 2 | (A A) | [dneg_elim_a] |