(4steps total) PrintForm DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub unit 1 1

1. x : Unit
   = x


By: UnitInd Hyp:1


Generated subgoals:

None

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

(4steps total) PrintForm DiscreteMath Sections DiscrMathExt Doc