IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hlength nil 2 'a:S. all(l:hlist('a). equal(equal(length(l),0),equal(l,nil)))
By:
HOL "hlength_nil_2"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a:S. all(
l:hlist('a). equal(equal(length(l),0),equal(l,nil)))
