Nuprl - Proof: hnot nil cons

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hnot nil cons

'a:S. all(

t:hlist('a). all(

h:'a. not(equal(nil,cons(h,t)))))

By:	HOL "hnot_nil_cons"

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html