(2steps total) PrintForm Definitions hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: heta ax 1
1. 'b : S
2. 'a : S
3. t : 'a'b
  (x:'a. t(x)) = t
By: SwapEquands 0 THEN Simpsetp [`ext`] THEN StrongAuto

Generated subgoals:

None

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

(2steps total) PrintForm Definitions hol bool Sections HOLlib Doc