PrintForm
Definitions
hol
combin
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hs
def
'c
,
'b
,
'a
:S. equal(s,
f
:
'a
'b
'c
.
g
:
'a
'b
.
x
:
'a
.
f
(
x
,
g
(
x
)))
By:
Simpsetp [`hol_to_nuprl`] THEN StrongAuto
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
'c,'b,'a:S. equal(s,
f:'a 
'b 'c. g:'a 'b. x:'a. f(x,g(x))) 'c,'b,'a:S. equal(s,f:'a 'b 'c. g:'a 'b. x:'a. f(x,g(x)))
