At:
list-list-connect-append2
For any graph
A,B,C:V List. A-- > *C 
B-- > *C 
A @ B-- > *C
By:
Unfold `list-list-connect` 0
THEN
Unfold `l_all` 0
THEN
Unfold `list-connect` 0
THEN
Unfold `l_exists` 0
THEN
SplitOrHyps
THEN
FwdThru -3 [-1]
THEN
ParallelOp -1
THEN
RWO
Thm* x:T, l1,l2:T List. (x 
l1 @ l2) 
(x l1) (x l2)
0
THEN
Obvious
Generated subgoals:
None
About:
