Def  A & B == AB

is mentioned by

Thm*  B:Prop(given A). (A & B)  Prop	[cand_is_prop]
Thm*  Q:Prop(given P). Dec(P)  (P  Dec(Q))  Dec(P & Q)	[decidable__cand]

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