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

At: card fun vs nsub exp

  a,b:. (ab) ~ (ba)
By: Auto

Generated subgoal:

1 1. a : 
2. b : 
  (ab) ~ (ba)
1 step

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

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