PrintForm
Definitions
hol
combin
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hi
o
id
'b
,
'a
:S. all(
f
:
'a
'b
. and(equal(o(i,
f
),
f
),equal(o(
f
,i),
f
)))
By:
HOL "hi_o_id"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
hol
combin
Sections
HOLlib
Doc
'b,'a:S. all(
f:'a 
'b. and(equal(o(i,f),f),equal(o(f,i),f))) 'b,'a:S. all(f:'a 'b. and(equal(o(i,f),f),equal(o(f,i),f)))
