(4steps total) PrintForm Definitions hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eq pred marker wf 1 1
1. 'a : S
  <eq_pred:(x:'a. y:'a. x = y)>  'a'a
By: Unab [`eq_pred_marker`] THEN StrongAuto

Generated subgoals:

None

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

(4steps total) PrintForm Definitions hol Sections HOLlib Doc