PrintForm
Definitions
hol
sum
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
houtl
wd
'a
,
'b
:S. all(
x
:
'a
. equal(outl(inl(
x
)),
x
))
By:
Unab [`houtl`] THEN HN THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
hol
sum
Sections
HOLlib
Doc
'a,'b:S. all(
x:'a. equal(outl(inl(x)),x)) 'a,'b:S. all(x:'a. equal(outl(inl(x)),x))
