At:
list-list-connect-append
For any graph
A,B,C:V List. A-- > *B @ C 
A-- > *B & A-- > *C
By:
Unfold `list-list-connect` 0
THEN
Unfold `l_all` 0
THEN
Unfold `list-connect` 0
THEN
Unfold `l_exists` 0
THEN
All
(RWO
Thm* x:T, l1,l2:T List. (x 
l1 @ l2) (x l1) 
(x l2))
THEN
SplitOrHyps
THEN
EasyHyp
Generated subgoals:
None
About:
