Nuprl - Proof: happend wd

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

'a:S.

and

(all(

l:hlist('a). equal(append(nil,l),l))

,all

l1:hlist('a). all

l1:hlist('a). (

l2:hlist('a). all

l1:hlist('a). (

l2:hlist('a). (

h:'a. equal

l1:hlist('a). (

l2:hlist('a). (

h:'a. (append(cons(h,l1),l2)

l1:hlist('a). (

l2:hlist('a). (

h:'a. ,cons(h,append(l1,l2)))))))

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