At:
list-list-connect-iseg
For any graph
A,B:V List. B A A-- > *B
By:
Unfold `list-list-connect` 0
THEN
Unfold `l_all` 0
THEN
Unfold `list-connect` 0
THEN
Unfold `l_exists` 0
THEN
InstConcl [x]
THEN
FwdThru
Thm*l1,l2:T List, x:T. l1 l2 (x l1) (x l2)
[-3;-1]
THEN
Connect
Generated subgoals:
For any graph
A,B:V List. B 
A 
A-- > *B
l1)