Def  {i...} == {j:| ij }

is mentioned by

Thm*  P:(Prop).  Thm*  (a:, b:{...a}. P(a,b)) Thm*   Thm*  (a:, b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (a,b:. P(a,b))	[all_int_segs_by_upper_ind]
Thm*  P:(Prop), a:. Thm*  (b:{...a}. P(a,b)) Thm*   Thm*  (b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (b:. P(a,b))	[int_segs_from_base_by_upper_ind]
Thm*  P:(Prop), a:. Thm*  (b:{...a}. P(a,a)  P(a,b))  (b:{a...}. P(a,b))  (b:. P(a,b))	[split_int_domain_by_norm_lower]
Thm*  P:(Prop), a:. Thm*  (b:{a...}. (c:{a..b}. P(a,c))  P(a,b))  (b:{a...}. P(a,b))	[int_seg_upper_ind]
Thm*  P:(Prop).  Thm*  (a:, b:{...a}. P(a,b)) Thm*   Thm*  (a:. (b:{...a}. P(a,b))  (b:{a...}. P(a,b)))  (a,b:. P(a,b))	[all_int_pairs_via_all_splits]
Thm*  P:(Prop), a:. Thm*  (b:{...a}. P(a,b)) Thm*   Thm*  ((b:{...a}. P(a,b))  (b:{a...}. P(a,b)))  (b:. P(a,b))	[split_int_domain]

In prior sections: int 1 int 2 SimpleMulFacts

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html