IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  A == A  False

is mentioned by

Thm*  a,b:P:({a..b}Prop). ba  (i:{a..b}. P(i))[exist_intseg_null]

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

IteratedBinops Sections DiscrMathExt Doc