(13steps total) PrintForm Definitions Lemmas hol restr binder Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: harb wd 1 1 1 3
1. 'a : S
2. z : {'a:S}
  z  Type
By: Analyze 2 THEN StrongAuto

Generated subgoals:

None

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

(13steps total) PrintForm Definitions Lemmas hol restr binder Sections HOLlib Doc