Nuprl - Proof: concat append 2

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

1. (Top List) List
2. u : Top List
3. v : (Top List) List
4.

ll2:(Top List) List. concat(v @ ll2) ~ (concat(v) @ concat(ll2))
5. ll2 : (Top List) List

(u @ concat(v @ ll2)) ~ ((u @ concat(v)) @ concat(ll2))

By:	RWO Thm* as,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs) 0 THEN Analyze THEN Try BackThruSomeHyp

Generated subgoals:

None

About:

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