PrintForm
Definitions
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
bequal
wf
T
:Type,
x
,
y
:
T
. (
x
=
y
)
By:
Unfold `bequal` 0 THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
hol
Sections
HOLlib
Doc
T:Type, x,y:T. (x =
y) 
T:Type, x,y:T. (x = y) 
