Nuprl - Proof: hlength wd

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hlength wd

'a:S.

and

(equal(length(nil),0)

,all(

h:'a. all(

t:hlist('a). equal(length(cons(h,t)),suc(length(t))))))

By:	HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html