i,j:
, F:({i..j
}
Prop).
(k:{i..j}. Dec(F(k))) 
Dec(
k:{i..j}. F(k))i:, E:({...i}Prop).
E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))| Rank | Theorem | Name |
| 6 |
Thm* i,j:, F:({i..j}Prop).
(k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k)) | [decidable__ex_int_seg] |
| cites | ||
| 5 |
Thm* i:, E:({...i}Prop).
E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k)) | [int_lower_ind] |