is mentioned by

Thm*  a,b:, P:({a..b}Prop). (i:{a..b}. P(i))  (Or i:{a..b}. P(i))	[exist_intseg_vs_iter_or]
Thm*  a,b:, P:({a..b}Prop). ba  (i:{a..b}. P(i))	[exist_intseg_null]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i))  P(b-1))	[or_via_exist_intseg_split_last]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b Thm*   Thm*  (c:. b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i))  P(c)))	[or_via_exist_intseg_notnull]
Thm*  a,b:, P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i))	[all_intseg_vs_iter_and]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i)) & P(b-1))	[and_via_all_intseg_split_last]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b Thm*   Thm*  (c:. b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i)) & P(c)))	[and_via_all_intseg_notnull]
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]
Thm*  f:(AAA). is_commutative_sep(A; f)  Prop	[is_commutative_sep_wf]
Thm*  f:(AAA). is_commutative(A; x,z.f(x,z))  Prop	[is_commutative_wf]
Thm*  f:(AAA). is_assoc_sep(A; f)  Prop	[is_assoc_sep_wf]
Thm*  f:(AAA), u:A. is_ident(A; f; u)  Prop	[is_ident_wf]

In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2

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