'a:S, l1,l2,l3:'a List. (l1 @ l2 @ l3) = ((l1 @ l2) @ l3)

By:

RewriteOfThm Thm* 'a:S.  Thm* all Thm* (l1:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). equal Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). (append(l1,append(l2,l3)) Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,append Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,(append(l1,l2) Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,,l3))))) (SimpsetC [`hol_to_nuprl`;`bequal`])

None

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