(3steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hlet
def
'b
,
'a
:S. equal(let,
f
:
'a
'b
.
x
:
'a
.
f
(
x
))
By:
Simpset [`hol_to_nuprl`] THEN Simp THEN StrongAuto
Generated subgoal:
1
1.
'b
: S
2.
'a
: S
(
f
:
'a
'b
.
e
:
'a
. let
x
=
e
in
f
(
x
)) =
(
f
:
'a
'b
.
x
:
'a
.
f
(
x
))
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
'b,'a:S. equal(let,
f:'a 
'b. x:'a. f(x)) 'b,'a:S. equal(let,f:'a 'b. x:'a. f(x)) (f:'a'b. e:'a. let x = e in f(x)) =
(f:'a'b. x:'a. f(x))
