(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card sigma vs nsub sigma 1 2

1. b : 0
  0 ~ ( i:0. b(i))


By: Compute  i:0. b(i) * 0


Generated subgoals:

None

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

(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc