(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
'a
:S. equal(nil,abs_list(pair((
n
:hnum. select(
e
:
'a
. t)),0)))
By:
HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))
Generated subgoal:
1
1.
'a
: S
nil = abs_list(<
n
:hnum. @
e
:
'a
. true
,0>)
7
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
'a:S. equal(nil,abs_list(pair((
n:hnum. select(e:'a. t)),0))) 'a:S. equal(nil,abs_list(pair((n:hnum. select(e:'a. t)),0))) nil = abs_list(<n:hnum. @
e:'a. true
,0>)
