Nuprl - int_2 LEMMAs for decidable__ex_int

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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 the following:
5	Thm* i:, E:({...i}Prop). Thm* E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))	[int_lower_ind]
0	Thm* Dec(P) Dec(Q) Dec(P Q)	[decidable__or]
0	Thm* i,j:. Thm* i<j Thm* Thm* (F:({i..j}Prop). (k:{i..j}. F(k)) F(i) (k:{(i+1)..j}. F(k)))	[split_int_seg_exist_dom_sfa]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html