PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The size of the disjoint union of two finite classes is the sum of those classes' sizes.

At: nsub add rw

  a,b:. (a+b) ~ (a+b)
By: Auto THEN BackThru: Thm*  c,a,b:. a+b = c    ((a+b) ~ c)

Generated subgoals:

None

About:
natural_numberaddunionequalimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc