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

1. a : 
2. p : a
3. i : a
4. p(i)
  true  1 = 1  2


By: Compute true * True


Generated subgoals:

None

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

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