Def  P & Q == PQ

is mentioned by

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]
Def  is_ident(A; f; u) == x:A. f(u,x) = x & f(x,u) = x	[is_ident]

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

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