(4steps total) PrintForm hol min Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: function wf stype 1 1 1

1. 'a : {T:Type| x:T. True }
2. 'b : Type
3. 'b
4. True
  x:('a'b). True


By: DTerm (y.x) 0 THEN StrongAuto


Generated subgoals:

None

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

(4steps total) PrintForm hol min Sections HOLlib Doc