(6steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose iter id 1 1
1. A : Type
  Id{0} = Id  AA
By: BackThru: Thm*  f:(AA). f{0} = Id ...w

Generated subgoals:

None

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

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