Def  x:A. B(x) == x:AB(x)

is mentioned by

Thm*  (i:{a..b}. e(i) = 0)  ( i:{a..b}. e(i)) = 0	[zero_ann_iter_via_intseg]
Thm*  ( i:{a..b}. e(i)) = 0  (i:{a..b}. e(i) = 0)	[iter_prod_zero_iff_factor_zero]
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]

In prior sections: core quot 1 LogicSupplement int 2 num thy 1 SimpleMulFacts

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