Def  P  Q == P+Q

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). 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*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,b:, c:{a...b}, d:{c..b}, e:({a..b}A). Thm*  ((i:{a..b}. i<c  di  e(i) = u) Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{c..d}. e(i)))	[iter_via_intseg_amputate_units]

In prior sections: core bool 1 rel 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