(2steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inj typing imp le 1

1. m : 
2. k : 
3. f : {f:(mk)| Inj(mkf) }
  Inj(mkf)


By: Analyze-1 THEN Unhide


Generated subgoals:

None

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

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