Nuprl - Proof: happend assoc 2

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

'a:S.

all

(

l1:hlist('a). all

(

l1:hlist('a). (

l2:hlist('a). all

(

l1:hlist('a). (

l2:hlist('a). (

l3:hlist('a). equal

(

l1:hlist('a). (

l2:hlist('a). (

l3:hlist('a). (append(l1,append(l2,l3))

(

l1:hlist('a). (

l2:hlist('a). (

l3:hlist('a). ,append(append(l1,l2),l3)))))

By:	HOL "happend_assoc_2"

Generated subgoals:

None

About:

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