(8steps total)
PrintForm
Definitions
Lemmas
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hnil
def
1
2
1
1
1.
'a
: S
(
n
:
. if
n
<
0 then nil[
n
] else arb(
'a
) fi ) = (
n
:
. @
e
:
'a
. true
)
By:
Analyze THEN StrongAuto THEN Try (Complete (Unfold `label` 0))
Generated subgoal:
1
2.
n
:
if
n
<
0 then nil[
n
] else arb(
'a
) fi = (@
e
:
'a
. true
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
Lemmas
hol
list
1
Sections
HOLlib
Doc
(
n:
. if n<
0 then nil[n] else arb('a) fi ) = (
e:'a. true
