IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq pred marker wf12 1. 'a : S
<eq_pred:(x:'a. y:'a. x =y)> = (x:'a. y:'a. x =y) 'a'a
By:
Unab [`eq_pred_marker`] THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
<eq_pred:(
x:'a. 
y)> = (
'a
'a
