Nuprl - Proof: hnot cons nil

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

'a:S. all(

t:hlist('a). all(

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

By:	HOL "hnot_cons_nil"

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